Module Tacticals.New
The tacticals in the module New
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.New
, but they are more atomic. In particular Tacticals.New.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).
val catch_failerror : Exninfo.iexn -> unit Proofview.tactic
catch_failerror e
fails and decreases the level ife
is an Ltac error with level more than 0. Otherwise succeeds.
val tclIDTAC : unit Proofview.tactic
val tclTHEN : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclFAIL : ?info:Exninfo.info -> int -> Pp.t -> 'a Proofview.tactic
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.
val tclONCE : unit Proofview.tactic -> unit Proofview.tactic
val 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 tactictac1
togls
then, appliest1
, ...,tn
to the firstn
resulting subgoals,t'1
, ...,t'm
to the lastm
subgoals andtac2
to the rest of the subgoals in the middle. Raises an error if the number of resulting subgoals is strictly less thann+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 tactictac1
togls
andtac2
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
val tclTHENLIST : unit Proofview.tactic list -> unit Proofview.tactic
val tclMAP : ('a -> unit Proofview.tactic) -> 'a list -> unit Proofview.tactic
tclMAP f [x1..xn]
builds(f x1);(f x2);...(f xn)
val tclTRY : unit Proofview.tactic -> unit Proofview.tactic
val tclTRYb : unit Proofview.tactic -> bool list Proofview.tactic
val 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
val tclDO : int -> unit Proofview.tactic -> unit Proofview.tactic
val tclREPEAT : unit Proofview.tactic -> unit Proofview.tactic
val tclREPEAT_MAIN : unit Proofview.tactic -> unit Proofview.tactic
val tclCOMPLETE : 'a Proofview.tactic -> 'a Proofview.tactic
val tclSOLVE : unit Proofview.tactic list -> unit Proofview.tactic
val tclPROGRESS : unit Proofview.tactic -> unit Proofview.tactic
val tclSELECT : Goal_select.t -> 'a Proofview.tactic -> 'a 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 tclTIMEOUT : int -> unit Proofview.tactic -> unit Proofview.tactic
val tclTIME : string option -> 'a Proofview.tactic -> 'a Proofview.tactic
val 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 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
val 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
val elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family
val 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
val elimination_then : (branch_args -> unit Proofview.tactic) -> EConstr.constr -> unit Proofview.tactic
val case_then_using : Tactypes.or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> EConstr.constr option -> (Names.inductive * EConstr.EInstance.t) -> (EConstr.constr * EConstr.types) -> unit Proofview.tactic
val case_nodep_then_using : Tactypes.or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> EConstr.constr option -> (Names.inductive * EConstr.EInstance.t) -> (EConstr.constr * EConstr.types) -> unit Proofview.tactic
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val pf_constr_of_global : Names.GlobRef.t -> EConstr.constr Proofview.tactic