[api] Move some types to their proper module.

We solve some modularity and type duplication problems by moving types
to a better place. In particular:

- We move tactics types from `Misctypes` to `Tactics` as this is their
  proper module an single user [with LTAC].

- We deprecate aliases in `Tacexpr` to such tactic types.

cc: #6512

1 files changed, 7 insertions, 0 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0d9f3d821..d0ec3358a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1159,6 +1159,13 @@ let tactic_infer_flags with_evar = {
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
 
+type 'a core_destruction_arg =
+  | ElimOnConstr of 'a
+  | ElimOnIdent of lident
+  | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+  clear_flag * 'a core_destruction_arg
 
 let onOpenInductionArg env sigma tac = function
   | clear_flag,ElimOnConstr f ->