(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* tactic val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic val tclTHENSEQ : tactic list -> tactic val tclTHENLIST : tactic list -> tactic val tclTHEN_i : tactic -> (int -> tactic) -> tactic val tclTHENFIRST : tactic -> tactic -> tactic val tclTHENLAST : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic val tclTHENSV : tactic -> tactic array -> tactic val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic val tclTHENFIRSTn : tactic -> tactic array -> tactic val tclREPEAT : tactic -> tactic val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> std_ppcmds -> tactic val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic val tclFIRST_PROGRESS_ON : ('a -> tactic) -> 'a list -> tactic (** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (Id.t -> tactic) -> tactic val onNthHyp : int -> (constr -> tactic) -> tactic val onNthDecl : int -> (named_declaration -> tactic) -> tactic val onLastHypId : (Id.t -> tactic) -> tactic val onLastHyp : (constr -> tactic) -> tactic val onLastDecl : (named_declaration -> tactic) -> tactic val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic val onNLastHyps : int -> (constr list -> tactic) -> tactic val onNLastDecls : int -> (named_context -> tactic) -> tactic val lastHypId : goal sigma -> Id.t val lastHyp : goal sigma -> constr val lastDecl : goal sigma -> named_declaration val nLastHypsId : int -> goal sigma -> Id.t list val nLastHyps : int -> goal sigma -> constr list val nLastDecls : int -> goal sigma -> named_context val afterHyp : Id.t -> goal sigma -> named_context val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> tactic) -> (Id.t -> tactic) -> Id.t -> tactic val onHyps : (goal sigma -> named_context) -> (named_context -> tactic) -> tactic (** {6 Tacticals applying to goal components } *) (** A [clause] denotes occurrences and hypotheses in a goal; in particular, it can abstractly refer to the set of hypotheses independently of the effective contents of the current goal *) val tryAllHyps : (Id.t -> tactic) -> tactic val tryAllHypsAndConcl : (Id.t option -> tactic) -> tactic val onAllHyps : (Id.t -> tactic) -> tactic val onAllHypsAndConcl : (Id.t option -> tactic) -> tactic val onClause : (Id.t option -> tactic) -> clause -> tactic val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) type branch_args = { ity : inductive; (** the type we were eliminating on *) largs : constr list; (** its arguments *) branchnum : int; (** the branch number *) pred : constr; (** the predicate we used *) nassums : int; (** the number of assumptions to be introduced *) branchsign : bool list; (** the signature of the branch. true=recursive argument, false=constant *) branchnames : intro_pattern_expr located list} type branch_assumptions = { ba : branch_args; (** the branch args *) assums : named_context} (** the list of assumptions introduced *) (** [check_disjunctive_pattern_size loc pats n] returns an appropriate error message if |pats| <> n *) val check_or_and_pattern_size : Loc.t -> or_and_intro_pattern_expr -> int -> unit (** Tolerate "[]" to mean a disjunctive pattern of any length *) val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr -> or_and_intro_pattern_expr (** Useful for [as intro_pattern] modifier *) val compute_induction_names : int -> intro_pattern_expr located option -> intro_pattern_expr located list array val elimination_sort_of_goal : goal sigma -> sorts_family val elimination_sort_of_hyp : Id.t -> goal sigma -> sorts_family val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family val general_elim_then_using : (inductive -> goal sigma -> constr) -> rec_flag -> intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic val elimination_then_using : (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> constr -> tactic val elimination_then : (branch_args -> tactic) -> (arg_bindings * arg_bindings) -> constr -> tactic val case_then_using : intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic val case_nodep_then_using : intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic val simple_elimination_then : (branch_args -> tactic) -> constr -> tactic val elim_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic val case_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic (** Tacticals defined directly in term of Proofview *) (** 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 like 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). *) module New : sig open Proofview (** [catch_failerror e] fails and decreases the level if [e] is an Ltac error with level more than 0. Otherwise succeeds. *) val catch_failerror : exn -> unit tactic val tclTHEN : unit tactic -> unit tactic -> unit tactic (* [tclFAIL n msg] fails with [msg] as an error message at level [n] (meaning that it will jump over [n] error catching tacticals FROM THIS MODULE. *) val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic val tclOR : unit tactic -> unit tactic -> unit tactic val tclONCE : unit tactic -> unit tactic val tclEXACTLY_ONCE : unit tactic -> unit tactic val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit 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 tclTHENS3PARTS : unit tactic -> unit tactic array -> unit tactic -> unit tactic array -> unit tactic val tclTHENSFIRSTn : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclTHENFIRSTn : unit tactic -> unit tactic array -> unit tactic (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the first resulting subgoal *) val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic val tclTHENLASTn : unit tactic -> unit tactic array -> unit tactic val tclTHENLAST : unit tactic -> unit tactic -> unit tactic (* [tclTHENS t l = t <*> tclDISPATCH l] *) val tclTHENS : unit tactic -> unit tactic list -> unit tactic (* [tclTHENLIST [t1;…;tn]] is [t1<*>…<*>tn] *) val tclTHENLIST : unit tactic list -> unit tactic (** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic val tclTRY : unit tactic -> unit tactic val tclFIRST : unit tactic list -> unit tactic val tclFIRST_PROGRESS_ON : ('a -> unit tactic) -> 'a list -> unit tactic val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic val tclDO : int -> unit tactic -> unit tactic val tclREPEAT : unit tactic -> unit tactic (* Repeat on the first subgoal (no failure if no more subgoal) *) val tclREPEAT_MAIN : unit tactic -> unit tactic val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic val tclTIMEOUT : int -> unit tactic -> unit tactic val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> identifier -> unit Proofview.tactic val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic val onLastHypId : (identifier -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic val tryAllHyps : (identifier -> unit tactic) -> unit tactic val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic val onClause : (identifier option -> unit tactic) -> clause -> unit tactic val elimination_then : (branch_args -> unit Proofview.tactic) -> (arg_bindings * arg_bindings) -> constr -> unit Proofview.tactic val case_then_using : intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> unit Proofview.tactic val case_nodep_then_using : intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> 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 end