diff options
Diffstat (limited to 'plugins/ltac/tacexpr.ml')
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 3baa475ab..d51de8c65 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,7 +35,8 @@ 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 | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -74,7 +75,7 @@ type 'id message_token = type ('dconstr,'id) induction_clause = 'dconstr with_bindings Tactics.destruction_arg * - (intro_pattern_naming_expr CAst.t option (* eqn:... *) + (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 ... *) @@ -116,7 +117,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 @@ -133,7 +134,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 *) @@ -151,7 +152,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 @@ -163,7 +164,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" @@ -269,7 +270,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 Vernacexpr.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 *) @@ -304,7 +305,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 |