[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

5 files changed, 30 insertions, 5 deletions

diff --git a/tactics/equality.mli b/tactics/equality.mli
index c0be917a0..ccf454c3e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -80,20 +80,20 @@ val discrConcl   : unit Proofview.tactic
 val discrHyp     : Id.t -> unit Proofview.tactic
 val discrEverywhere : evars_flag -> unit Proofview.tactic
 val discr_tac    : evars_flag ->
-  constr with_bindings destruction_arg option -> unit Proofview.tactic
+  constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
 
 (* Below, if flag is [None], it takes the value from the dynamic value of the option *)
 val inj          : inj_flags option -> intro_patterns option -> evars_flag ->
   clear_flag -> constr with_bindings -> unit Proofview.tactic
 val injClause    : inj_flags option -> intro_patterns option -> evars_flag ->
-  constr with_bindings destruction_arg option -> unit Proofview.tactic
+  constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
 val injHyp       : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic
 val injConcl     : inj_flags option -> unit Proofview.tactic
 val simpleInjClause : inj_flags option -> evars_flag ->
-  constr with_bindings destruction_arg option -> unit Proofview.tactic
+  constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
 
-val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
+val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic
 
 val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 067fc8941..d76c9a697 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -64,6 +64,11 @@ let var_occurs_in_pf gl id =
 
 type inversion_status = Dep of constr option | NoDep
 
+type inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear
+
 let compute_eqn env sigma n i ai =
   (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
 
diff --git a/tactics/inv.mli b/tactics/inv.mli
index c63d57af5..9d4ffdd7b 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -15,6 +15,11 @@ open Tactypes
 
 type inversion_status = Dep of constr option | NoDep
 
+type inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear
+
 val inv_clause :
   inversion_kind -> or_and_intro_pattern option -> Id.t list ->
     quantified_hypothesis -> unit Proofview.tactic
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 ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 079baa3ef..7809dbf48 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -95,6 +95,14 @@ val try_intros_until :
 (** Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
+type 'a core_destruction_arg =
+  | ElimOnConstr of 'a
+  | ElimOnIdent of lident
+  | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+  clear_flag * 'a core_destruction_arg
+
 val onInductionArg :
   (clear_flag -> constr with_bindings -> unit Proofview.tactic) ->
     constr with_bindings destruction_arg -> unit Proofview.tactic