package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Elimination tacticals.

The Coq Proof Assistant -- Core Binaries and Tools

Install

dune-project

Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.2.tar.gz

md5=5d1187d5e44ed0163f76fb12dabf012e

sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

doc/coq-core.tactics/Tacticals/index.html

Module `Tacticals`Source

Sourceexception FailError of int * Pp.t Lazy.t

A special exception for levels for the Fail tactic

Tacticals defined directly in term of Proofview

The tacticals below are the tactical of Ltac. Their semantics is an extension of the tacticals in this file for the multi-goal backtracking tactics. They do not have the same semantics as the similarly named tacticals in Proofview. The tactical of Proofview are used in the definition of the tacticals of Tacticals, but they are more atomic. In particular Tacticals.tclORELSE sees lack of progress as a failure, whereas Proofview.tclORELSE doesn't. Additionally every tactic which can catch failure (tclOR, tclORELSE, tclTRY, tclREPEAt, etc…) are run into each goal independently (failures and backtracks are localised to a given goal).

Sourceval catch_failerror : Exninfo.iexn -> unit Proofview.tactic

catch_failerror e fails and decreases the level if e is an Ltac error with level more than 0. Otherwise succeeds.

Sourceval tclIDTAC : unit Proofview.tactic

val tclTHEN : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

Sourceval tclFAILn : ?info:Exninfo.info -> int -> Pp.t -> 'a Proofview.tactic

Sourceval tclFAIL : ?info:Exninfo.info -> Pp.t -> 'a Proofview.tactic

Same as above with level set to 0.

val tclZEROMSG : 
  ?info:Exninfo.info ->
  ?loc:Loc.t ->
  Pp.t ->
  'a Proofview.tactic

Fail with a User_Error containing the given message.

val tclOR : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclORD : 
  unit Proofview.tactic ->
  (unit -> unit Proofview.tactic) ->
  unit Proofview.tactic

Like tclOR but accepts a delayed tactic as a second argument in the form of a function which will be run only in case of backtracking.

Sourceval tclONCE : unit Proofview.tactic -> unit Proofview.tactic

Sourceval tclEXACTLY_ONCE : unit Proofview.tactic -> unit Proofview.tactic

val tclIFCATCH : 
  unit Proofview.tactic ->
  (unit -> unit Proofview.tactic) ->
  (unit -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tclORELSE0 : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclORELSE : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclTHENS3PARTS : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic

tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls applies the tactic tac1 to gls then, applies t1, ..., tn to the first n resulting subgoals, t'1, ..., t'm to the last m subgoals and tac2 to the rest of the subgoals in the middle. Raises an error if the number of resulting subgoals is strictly less than n+m

val tclTHENSLASTn : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic

val tclTHENSFIRSTn : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclTHENFIRSTn : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic

val tclTHENFIRST : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

tclTHENFIRST tac1 tac2 gls applies the tactic tac1 to gls and tac2 to the first resulting subgoal

val tclBINDFIRST : 
  'a Proofview.tactic ->
  ('a -> 'b Proofview.tactic) ->
  'b Proofview.tactic

val tclTHENLASTn : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic

val tclTHENLAST : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclBINDLAST : 
  'a Proofview.tactic ->
  ('a -> 'b Proofview.tactic) ->
  'b Proofview.tactic

val tclTHENS : 
  unit Proofview.tactic ->
  unit Proofview.tactic list ->
  unit Proofview.tactic

Sourceval tclTHENLIST : unit Proofview.tactic list -> unit Proofview.tactic

Sourceval tclMAP : ('a -> unit Proofview.tactic) -> 'a list -> unit Proofview.tactic

tclMAP f [x1..xn] builds (f x1);(f x2);...(f xn)

Sourceval tclTRY : unit Proofview.tactic -> unit Proofview.tactic

Sourceval tclTRYb : unit Proofview.tactic -> bool list Proofview.tactic

Sourceval tclFIRST : unit Proofview.tactic list -> unit Proofview.tactic

val tclIFTHENELSE : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclIFTHENSVELSE : 
  unit Proofview.tactic ->
  unit Proofview.tactic array ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclIFTHENTRYELSEMUST : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val tclIFTHENFIRSTTRYELSEMUST : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

Sourceval tclDO : int -> unit Proofview.tactic -> unit Proofview.tactic

Sourceval tclREPEAT : unit Proofview.tactic -> unit Proofview.tactic

Sourceval tclREPEAT_MAIN : unit Proofview.tactic -> unit Proofview.tactic

Sourceval tclCOMPLETE : 'a Proofview.tactic -> 'a Proofview.tactic

Sourceval tclSOLVE : unit Proofview.tactic list -> unit Proofview.tactic

Sourceval tclPROGRESS : unit Proofview.tactic -> unit Proofview.tactic

val tclWITHHOLES : 
  bool ->
  'a Proofview.tactic ->
  Evd.evar_map ->
  'a Proofview.tactic

val tclDELAYEDWITHHOLES : 
  bool ->
  'a Tactypes.delayed_open ->
  ('a -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tclMAPDELAYEDWITHHOLES : 
  bool ->
  'a Tactypes.delayed_open list ->
  ('a -> unit Proofview.tactic) ->
  unit Proofview.tactic

Sourceval tclTIMEOUT : int -> unit Proofview.tactic -> unit Proofview.tactic

Sourceval tclTIME : string option -> 'a Proofview.tactic -> 'a Proofview.tactic

Sourceval nLastDecls : Proofview.Goal.t -> int -> EConstr.named_context

val ifOnHyp : 
  (Environ.env -> Evd.evar_map -> (Names.Id.t * EConstr.types) -> bool) ->
  (Names.Id.t -> unit Proofview.tactic) ->
  (Names.Id.t -> unit Proofview.tactic) ->
  Names.Id.t ->
  unit Proofview.tactic

val onNthHypId : 
  int ->
  (Names.Id.t -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onLastHypId : 
  (Names.Id.t -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onLastHyp : 
  (EConstr.constr -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onLastDecl : 
  (EConstr.named_declaration -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onNLastHypsId : 
  int ->
  (Names.Id.t list -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onNLastHyps : 
  int ->
  (EConstr.constr list -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onNLastDecls : 
  int ->
  (EConstr.named_context -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onHyps : 
  (Proofview.Goal.t -> EConstr.named_context) ->
  (EConstr.named_context -> unit Proofview.tactic) ->
  unit Proofview.tactic

val afterHyp : 
  Names.Id.t ->
  (EConstr.named_context -> unit Proofview.tactic) ->
  unit Proofview.tactic

Sourceval tryAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic

val tryAllHypsAndConcl : 
  (Names.Id.t option -> unit Proofview.tactic) ->
  unit Proofview.tactic

val onClause : 
  (Names.Id.t option -> unit Proofview.tactic) ->
  Locus.clause ->
  unit Proofview.tactic

Sourceval onAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic

val onAllHypsAndConcl : 
  (Names.Id.t option -> unit Proofview.tactic) ->
  unit Proofview.tactic

Sourceval elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family

Sourceval elimination_sort_of_hyp : Names.Id.t -> Proofview.Goal.t -> Sorts.family

val elimination_sort_of_clause : 
  Names.Id.t option ->
  Proofview.Goal.t ->
  Sorts.family

Sourceval pf_constr_of_global : Names.GlobRef.t -> EConstr.constr Proofview.tactic

val tclTYPEOFTHEN : 
  ?refresh:bool ->
  EConstr.constr ->
  (Evd.evar_map -> EConstr.types -> unit Proofview.tactic) ->
  unit Proofview.tactic

val tclSELECT : 
  ?nosuchgoal:'a Proofview.tactic ->
  Goal_select.t ->
  'a Proofview.tactic ->
  'a Proofview.tactic

deprecated Use [Goal_select.tclSELECT]

Elimination tacticals.

val get_and_check_or_and_pattern : 
  ?loc:Loc.t ->
  Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr ->
  bool list array ->
  Tactypes.intro_patterns array

get_and_check_or_and_pattern loc pats branchsign returns an appropriate error message if |pats| <> |branchsign|; extends them if no pattern is given for let-ins in the case of a conjunctive pattern

val fix_empty_or_and_pattern : 
  int ->
  Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr ->
  Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr

Tolerate "" to mean a disjunctive pattern of any length

val compute_constructor_signatures : 
  Environ.env ->
  rec_flag:bool ->
  (Names.inductive * 'a) ->
  bool list array

val compute_induction_names : 
  bool ->
  bool list array ->
  Tactypes.or_and_intro_pattern option ->
  Tactypes.intro_patterns array

Useful for as intro_pattern modifier

On This Page

Elimination tacticals.