diff options
Diffstat (limited to 'plugins/ltac/tacexpr.ml')
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 54 |
1 files changed, 35 insertions, 19 deletions
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 8b0c4404..11d13d3a 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -15,7 +15,7 @@ open Libnames open Genredexpr open Genarg open Pattern -open Misctypes +open Tactypes open Locus type ltac_constant = KerName.t @@ -35,30 +35,46 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Vernacexpr.goal_selector = +type goal_selector = Goal_select.t = + | SelectAlreadyFocused + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectNth of int + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectList of (int * int) list + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectId of Id.t + [@ocaml.deprecated "Use constructors in [Goal_select]"] | SelectAll + [@ocaml.deprecated "Use constructors in [Goal_select]"] +[@@ocaml.deprecated "Use [Goal_select.t]"] -type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = +type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a + [@ocaml.deprecated "Use constructors in [Tactics]"] | ElimOnIdent of lident + [@ocaml.deprecated "Use constructors in [Tactics]"] | ElimOnAnonHyp of int + [@ocaml.deprecated "Use constructors in [Tactics]"] +[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = - clear_flag * 'a core_destruction_arg + clear_flag * 'a Tactics.core_destruction_arg +[@@ocaml.deprecated "Use Tactics.destruction_arg"] -type inversion_kind = Misctypes.inversion_kind = +type inversion_kind = Inv.inversion_kind = | SimpleInversion + [@ocaml.deprecated "Use constructors in [Inv]"] | FullInversion + [@ocaml.deprecated "Use constructors in [Inv]"] | FullInversionClear + [@ocaml.deprecated "Use constructors in [Inv]"] +[@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -69,8 +85,8 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + 'dconstr with_bindings Tactics.destruction_arg * + (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -112,7 +128,7 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Tactypes.glob_constr_and_expr +type glob_constr_and_expr = Genintern.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr @@ -129,7 +145,7 @@ type delayed_open_constr = EConstr.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t (** Generic expressions for atomic tactics *) @@ -147,7 +163,7 @@ type 'a gen_atomic_tactic_expr = 'dtrm intro_pattern_expr CAst.t option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_naming_expr CAst.t option + Namegen.intro_pattern_naming_expr CAst.t option (* Derived basic tactics *) | TacInductionDestruct of @@ -159,7 +175,7 @@ type 'a gen_atomic_tactic_expr = (* Equality and inversion *) | TacRewrite of evars_flag * - (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * + (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * (* spiwack: using ['dtrm] here is a small hack, may not be stable by a change in the representation of delayed terms. Because, in fact, it is the whole "with_bindings" @@ -265,7 +281,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of goal_selector * 'a gen_tactic_expr + | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) @@ -300,7 +316,7 @@ constraint 'a = < type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference and_short_name or_var +type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -328,8 +344,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -393,5 +409,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) |