Tacticalsexception FailError of int * Pp.t Stdlib.Lazy.tA 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).
val catch_failerror : Exninfo.iexn -> unit Proofview.tacticcatch_failerror e fails and decreases the level if e is an Ltac error with level more than 0. Otherwise succeeds.
val tclIDTAC : unit Proofview.tacticval tclTHEN : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tacticval tclFAILn : ?info:Exninfo.info -> int -> Pp.t -> 'a Proofview.tacticval tclFAIL : ?info:Exninfo.info -> Pp.t -> 'a Proofview.tacticSame as above with level set to 0.
val tclZEROMSG : ?info:Exninfo.info -> ?loc:Loc.t -> Pp.t -> 'a Proofview.tacticFail with a User_Error containing the given message.
val tclOR : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tacticval tclORD : unit Proofview.tactic -> (unit -> unit Proofview.tactic) -> unit Proofview.tacticLike 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.tacticval tclEXACTLY_ONCE : unit Proofview.tactic -> unit Proofview.tacticval tclIFCATCH : unit Proofview.tactic -> (unit -> unit Proofview.tactic) -> (unit -> unit Proofview.tactic) -> unit Proofview.tacticval tclORELSE0 : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tacticval tclORELSE : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tacticval tclTHENS3PARTS : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactictclTHENS3PARTS 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.tacticval tclTHENSFIRSTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tacticval tclTHENFIRSTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tacticval tclTHENFIRST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactictclTHENFIRST 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.tacticval tclTHENLASTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tacticval tclTHENLAST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tacticval tclBINDLAST : 'a Proofview.tactic -> ('a -> 'b Proofview.tactic) -> 'b Proofview.tacticval tclTHENS : unit Proofview.tactic -> unit Proofview.tactic list -> unit Proofview.tacticval tclTHENLIST : unit Proofview.tactic list -> unit Proofview.tacticval tclMAP : ('a -> unit Proofview.tactic) -> 'a list -> unit Proofview.tactictclMAP f [x1..xn] builds (f x1);(f x2);...(f xn)
val tclTRY : unit Proofview.tactic -> unit Proofview.tacticval tclTRYb : unit Proofview.tactic -> bool list Proofview.tacticval tclFIRST : unit Proofview.tactic list -> unit Proofview.tacticval tclIFTHENELSE : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tacticval tclIFTHENSVELSE : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tacticval tclIFTHENTRYELSEMUST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tacticval tclIFTHENFIRSTTRYELSEMUST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tacticval tclDO : int -> unit Proofview.tactic -> unit Proofview.tacticval tclREPEAT : unit Proofview.tactic -> unit Proofview.tacticval tclREPEAT_MAIN : unit Proofview.tactic -> unit Proofview.tacticval tclCOMPLETE : 'a Proofview.tactic -> 'a Proofview.tacticval tclSOLVE : unit Proofview.tactic list -> unit Proofview.tacticval tclPROGRESS : unit Proofview.tactic -> unit Proofview.tacticval tclWITHHOLES : bool -> 'a Proofview.tactic -> Evd.evar_map -> 'a Proofview.tacticval tclDELAYEDWITHHOLES : bool -> 'a Tactypes.delayed_open -> ('a -> unit Proofview.tactic) -> unit Proofview.tacticval tclMAPDELAYEDWITHHOLES : bool -> 'a Tactypes.delayed_open list -> ('a -> unit Proofview.tactic) -> unit Proofview.tacticval check_evar_list : Environ.env -> Evd.evar_map -> Evar.Set.t -> Evd.evar_map -> Evar.t listval tclTIMEOUT : int -> unit Proofview.tactic -> unit Proofview.tacticval tclTIME : string option -> 'a Proofview.tactic -> 'a Proofview.tacticval nLastDecls : Proofview.Goal.t -> int -> EConstr.named_contextval 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.tacticval onNthHypId : int -> (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tacticval onLastHypId : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tacticval onLastHyp : (EConstr.constr -> unit Proofview.tactic) -> unit Proofview.tacticval onLastDecl : (EConstr.named_declaration -> unit Proofview.tactic) -> unit Proofview.tacticval onNLastHypsId : int -> (Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tacticval onNLastHyps : int -> (EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tacticval onNLastDecls : int -> (EConstr.named_context -> unit Proofview.tactic) -> unit Proofview.tacticval onHyps : (Proofview.Goal.t -> EConstr.named_context) -> (EConstr.named_context -> unit Proofview.tactic) -> unit Proofview.tacticval afterHyp : Names.Id.t -> (EConstr.named_context -> unit Proofview.tactic) -> unit Proofview.tacticval tryAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tacticval tryAllHypsAndConcl : (Names.Id.t option -> unit Proofview.tactic) -> unit Proofview.tacticval onClause : (Names.Id.t option -> unit Proofview.tactic) -> Locus.clause -> unit Proofview.tacticval onAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tacticval onAllHypsAndConcl : (Names.Id.t option -> unit Proofview.tactic) -> unit Proofview.tacticval elimination_sort_of_goal : Proofview.Goal.t -> Sorts.familyval elimination_sort_of_hyp : Names.Id.t -> Proofview.Goal.t -> Sorts.familyval elimination_sort_of_clause : Names.Id.t option -> Proofview.Goal.t -> Sorts.familyval pf_constr_of_global : Names.GlobRef.t -> EConstr.constr Proofview.tacticval tclTYPEOFTHEN : ?refresh:bool -> EConstr.constr -> (Evd.evar_map -> EConstr.types -> unit Proofview.tactic) -> unit Proofview.tacticval tclSELECT : ?nosuchgoal:'a Proofview.tactic -> Goal_select.t -> 'a Proofview.tactic -> 'a Proofview.tacticval 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 arrayget_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_exprTolerate "" to mean a disjunctive pattern of any length
val compute_constructor_signatures : Environ.env -> rec_flag:bool ->
(Names.inductive * 'a) -> bool list arrayval compute_induction_names : bool -> bool list array -> Tactypes.or_and_intro_pattern option -> Tactypes.intro_patterns arrayUseful for as intro_pattern modifier