diff options
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 108 |
1 files changed, 54 insertions, 54 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index cfdc2cff..f0ebac78 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -1,28 +1,31 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp open Names -open Term -open Tacmach +open Constr +open EConstr +open Evd open Proof_type -open Tacexpr open Locus open Misctypes +open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : std_ppcmds -> tactic +val tclIDTAC_MESSAGE : Pp.t -> tactic val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic val tclTHENSEQ : tactic list -> tactic +[@@ocaml.deprecated "alias of Tacticals.tclTHENLIST"] val tclTHENLIST : tactic list -> tactic val tclTHEN_i : tactic -> (int -> tactic) -> tactic val tclTHENFIRST : tactic -> tactic -> tactic @@ -40,13 +43,11 @@ 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 tclFAIL : int -> Pp.t -> tactic +val tclFAIL_lazy : int -> Pp.t 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 @@ -59,29 +60,29 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic val onNthHypId : int -> (Id.t -> tactic) -> tactic val onNthHyp : int -> (constr -> tactic) -> tactic -val onNthDecl : int -> (Context.Named.Declaration.t -> tactic) -> tactic +val onNthDecl : int -> (named_declaration -> tactic) -> tactic val onLastHypId : (Id.t -> tactic) -> tactic val onLastHyp : (constr -> tactic) -> tactic -val onLastDecl : (Context.Named.Declaration.t -> 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 -> (Context.Named.t -> tactic) -> tactic +val onNLastDecls : int -> (named_context -> tactic) -> tactic val lastHypId : goal sigma -> Id.t val lastHyp : goal sigma -> constr -val lastDecl : goal sigma -> Context.Named.Declaration.t +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 -> Context.Named.t +val nLastDecls : int -> goal sigma -> named_context -val afterHyp : Id.t -> goal sigma -> Context.Named.t +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 -> Context.Named.t) -> - (Context.Named.t -> tactic) -> tactic +val onHyps : (goal sigma -> named_context) -> + (named_context -> tactic) -> tactic (** {6 Tacticals applying to goal components } *) @@ -97,7 +98,7 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) -type branch_args = { +type branch_args = private { ity : pinductive; (** the type we were eliminating on *) largs : constr list; (** its arguments *) branchnum : int; (** the branch number *) @@ -107,15 +108,15 @@ type branch_args = { true=assumption, false=let-in *) branchnames : intro_patterns} -type branch_assumptions = { +type branch_assumptions = private { ba : branch_args; (** the branch args *) - assums : Context.Named.t} (** the list of assumptions introduced *) + assums : named_context} (** the list of assumptions introduced *) (** [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 get_and_check_or_and_pattern : - Loc.t -> delayed_open_constr or_and_intro_pattern_expr -> + ?loc:Loc.t -> delayed_open_constr or_and_intro_pattern_expr -> bool list array -> intro_patterns array (** Tolerate "[]" to mean a disjunctive pattern of any length *) @@ -123,22 +124,19 @@ val fix_empty_or_and_pattern : int -> delayed_open_constr or_and_intro_pattern_expr -> delayed_open_constr or_and_intro_pattern_expr -val compute_constructor_signatures : rec_flag -> pinductive -> bool list array +val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array (** Useful for [as intro_pattern] modifier *) val compute_induction_names : bool list array -> or_and_intro_pattern option -> intro_patterns 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 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 pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> 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 @@ -164,9 +162,9 @@ module New : sig (* [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 tclFAIL : int -> Pp.t -> 'a tactic - val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic + val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic (** Fail with a [User_Error] containing the given message. *) val tclOR : unit tactic -> unit tactic -> unit tactic @@ -209,10 +207,12 @@ module New : sig val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic val tclTRY : unit tactic -> unit tactic + val tclTRYb : unit tactic -> bool list tactic val tclFIRST : unit tactic 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 tclIFTHENFIRSTTRYELSEMUST : unit tactic -> unit tactic -> unit tactic val tclDO : int -> unit tactic -> unit tactic val tclREPEAT : unit tactic -> unit tactic @@ -221,35 +221,35 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : goal_selector -> 'a tactic -> 'a tactic + val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t + val nLastDecls : Proofview.Goal.t -> int -> named_context - val ifOnHyp : (identifier * types -> bool) -> - (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> - identifier -> unit Proofview.tactic + val ifOnHyp : (Id.t * types -> bool) -> + (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> + Id.t -> unit Proofview.tactic - val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic - val onLastHypId : (identifier -> unit tactic) -> unit tactic + val onNthHypId : int -> (Id.t -> unit tactic) -> unit tactic + val onLastHypId : (Id.t -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic - val onLastDecl : (Context.Named.Declaration.t -> unit tactic) -> unit tactic + val onLastDecl : (named_declaration -> unit tactic) -> unit tactic - val onHyps : ([ `NF ], Context.Named.t) Proofview.Goal.enter -> - (Context.Named.t -> unit tactic) -> unit tactic - val afterHyp : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic + val onHyps : (Proofview.Goal.t -> named_context) -> + (named_context -> unit tactic) -> unit tactic + val afterHyp : Id.t -> (named_context -> 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 tryAllHyps : (Id.t -> unit tactic) -> unit tactic + val tryAllHypsAndConcl : (Id.t option -> unit tactic) -> unit tactic + val onClause : (Id.t option -> unit tactic) -> clause -> unit tactic - val elimination_sort_of_goal : ('a, 'r) Proofview.Goal.t -> sorts_family - val elimination_sort_of_hyp : Id.t -> ('a, 'r) Proofview.Goal.t -> sorts_family - val elimination_sort_of_clause : Id.t option -> ('a, 'r) Proofview.Goal.t -> sorts_family + val elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family + val elimination_sort_of_hyp : Id.t -> Proofview.Goal.t -> Sorts.family + val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family val elimination_then : (branch_args -> unit Proofview.tactic) -> @@ -257,14 +257,14 @@ module New : sig val case_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic + constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic val case_nodep_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic + constr option -> inductive * EInstance.t -> constr * 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 : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic + val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic end |