[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, 0 insertions, 13 deletions

diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 9eb6f62cc3..72db3b31cb 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -142,19 +142,6 @@ type multi =
   | RepeatStar
   | RepeatPlus
 
-type 'a core_destruction_arg =
-  | ElimOnConstr of 'a
-  | ElimOnIdent of lident
-  | ElimOnAnonHyp of int
-
-type 'a destruction_arg =
-  clear_flag * 'a core_destruction_arg
-
-type inversion_kind =
-  | SimpleInversion
-  | FullInversion
-  | FullInversionClear
-
 type ('a, 'b) gen_universe_decl = {
   univdecl_instance : 'a; (* Declared universes *)
   univdecl_extensible_instance : bool; (* Can new universes be added *)