6 files changed, 29 insertions, 24 deletions
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 6637de745..434feba95 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -25,7 +25,7 @@ val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eva
 val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val uconstr : constr_expr Gram.entry
 val quantified_hypothesis : quantified_hypothesis Gram.entry
-val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
+val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
 val int_or_var : int or_var Gram.entry
 val simple_tactic : raw_tactic_expr Gram.entry
 val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5951f2b11..aea00c240 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -84,7 +84,7 @@ type pp_tactic = {
   pptac_prods : grammar_terminals;
 }
 
-val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t
+val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t
 
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index 5347eda7d..59473a5e5 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -23,7 +23,7 @@ val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_typ
 val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
 
 val wit_destruction_arg :
-  (constr_expr with_bindings Tacexpr.destruction_arg,
-   glob_constr_and_expr with_bindings Tacexpr.destruction_arg,
-   delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type
+  (constr_expr with_bindings Tactics.destruction_arg,
+   glob_constr_and_expr with_bindings Tactics.destruction_arg,
+   delayed_open_constr_with_bindings Tactics.destruction_arg) genarg_type
 
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 8b0c44041..3baa475ab 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector =
   | SelectList of (int * int) list
   | SelectId of Id.t
   | SelectAll
+[@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
 
-type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
+type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of lident
   | ElimOnAnonHyp of int
+[@@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
   | FullInversion
   | FullInversionClear
+[@@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,7 +73,7 @@ type 'id message_token =
   | MsgIdent of 'id
 
 type ('dconstr,'id) induction_clause =
-    'dconstr with_bindings destruction_arg *
+    'dconstr with_bindings Tactics.destruction_arg *
     (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 ... *)
@@ -265,7 +269,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 Vernacexpr.goal_selector * 'a gen_tactic_expr
   (* For ML extensions *)
   | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
   (* For syntax extensions *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 8b0c44041..3baa475ab 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector =
   | SelectList of (int * int) list
   | SelectId of Id.t
   | SelectAll
+[@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
 
-type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
+type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of lident
   | ElimOnAnonHyp of int
+[@@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
   | FullInversion
   | FullInversionClear
+[@@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,7 +73,7 @@ type 'id message_token =
   | MsgIdent of 'id
 
 type ('dconstr,'id) induction_clause =
-    'dconstr with_bindings destruction_arg *
+    'dconstr with_bindings Tactics.destruction_arg *
     (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 ... *)
@@ -265,7 +269,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 Vernacexpr.goal_selector * 'a gen_tactic_expr
   (* For ML extensions *)
   | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
   (* For syntax extensions *)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index bb815dcb3..105b5c59a 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -391,13 +391,10 @@ let explain_ltac_call_trace last trace loc =
 
 let skip_extensions trace =
   let rec aux = function
-  | (_,Tacexpr.LtacNameCall f as tac) :: _
-       when Tacenv.is_ltac_for_ml_tactic f -> [tac]
-  | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ ->
+  | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: tail ->
      (* Case of an ML defined tactic with entry of the form <<"foo" args>> *)
      (* see tacextend.mlp *)
-     [tac]
-  | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac]
+     tac :: aux tail
   | t :: tail -> t :: aux tail
   | [] -> [] in
   List.rev (aux (List.rev trace))