Module Tacticals

exception FailError of int * Pp.t Stdlib.Lazy.t

A special exception for levels for the Fail tactic

module Old : sig ... end
val 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.

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 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
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 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
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 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
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 onAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val onAllHypsAndConcl : (Names.Id.t option -> unit Proofview.tactic) -> 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 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
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