[api] Misctypes removal: move Tactypes to proofs

This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.

5 files changed, 15 insertions, 99 deletions

diff --git a/interp/genintern.ml b/interp/genintern.ml
index 161201c44..d9a0db040 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -26,9 +26,15 @@ let empty_glob_sign env = {
   extra = Store.empty;
 }
 
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+   in the environment by the effective calls to Intro, Inversion, etc
+   The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
-type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 module InternObj =
 struct
diff --git a/interp/genintern.mli b/interp/genintern.mli
index d818713fc..f4f064bca 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -22,6 +22,12 @@ type glob_sign = {
 
 val empty_glob_sign : Environ.env -> glob_sign
 
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+   in the environment by the effective calls to Intro, Inversion, etc
+   The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
 (** {5 Internalization functions} *)
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
@@ -42,7 +48,7 @@ val generic_substitute : glob_generic_argument subst_fun
 
 (** {5 Notation functions} *)
 
-type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun
 
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index e5ed58be6..7a7bb9a84 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -34,9 +34,6 @@ let wit_pre_ident : string uniform_genarg_type =
 let wit_int_or_var =
   make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
 
-let wit_intro_pattern =
-  make0 "intropattern"
-
 let wit_ident =
   make0 "ident"
 
@@ -45,8 +42,6 @@ let wit_var =
 
 let wit_ref = make0 "ref"
 
-let wit_quant_hyp = make0 "quant_hyp"
-
 let wit_sort_family = make0 "sort_family"
 
 let wit_constr =
@@ -56,12 +51,6 @@ let wit_uconstr = make0 "uconstr"
 
 let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
 
-let wit_constr_with_bindings = make0 "constr_with_bindings"
-
-let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
-
-let wit_bindings = make0 "bindings"
-
 let wit_red_expr = make0 "redexpr"
 
 let wit_clause_dft_concl  =
@@ -74,6 +63,4 @@ let wit_preident = wit_pre_ident
 let wit_reference = wit_ref
 let wit_global = wit_ref
 let wit_clause = wit_clause_dft_concl
-let wit_quantified_hypothesis = wit_quant_hyp
-let wit_intropattern = wit_intro_pattern
 let wit_redexpr = wit_red_expr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index dc9c370a1..4159e6054 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -18,8 +18,8 @@ open Genredexpr
 open Pattern
 open Constrexpr
 open Misctypes
-open Tactypes
 open Genarg
+open Genintern
 
 val wit_unit : unit uniform_genarg_type
 
@@ -35,16 +35,12 @@ val wit_pre_ident : string uniform_genarg_type
 
 val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
-val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
-
 val wit_ident : Id.t uniform_genarg_type
 
 val wit_var : (lident, lident, Id.t) genarg_type
 
 val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
 
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-
 val wit_sort_family : (Sorts.family, unit, unit) genarg_type
 
 val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
@@ -54,21 +50,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_
 val wit_open_constr :
   (constr_expr, glob_constr_and_expr, constr) genarg_type
 
-val wit_constr_with_bindings :
-  (constr_expr with_bindings,
-  glob_constr_and_expr with_bindings,
-  constr with_bindings delayed_open) genarg_type
-
-val wit_open_constr_with_bindings :
-  (constr_expr with_bindings,
-  glob_constr_and_expr with_bindings,
-  constr with_bindings delayed_open) genarg_type
-
-val wit_bindings :
-  (constr_expr bindings,
-  glob_constr_and_expr bindings,
-  constr bindings delayed_open) genarg_type
-
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
@@ -83,8 +64,6 @@ val wit_preident : string uniform_genarg_type
 val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
 val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
 val wit_clause :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
-val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
 val wit_redexpr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
diff --git a/interp/tactypes.ml b/interp/tactypes.ml
deleted file mode 100644
index f19abefee..000000000
--- a/interp/tactypes.ml
+++ /dev/null
@@ -1,62 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Tactic-related types that are not totally Ltac specific and still used in
-    lower API. It's not clear whether this is a temporary API or if this is
-    meant to stay. *)
-
-open Names
-open Constrexpr
-open Pattern
-
-(** Introduction patterns *)
-
-type 'constr intro_pattern_expr =
-  | IntroForthcoming of bool
-  | IntroNaming of Namegen.intro_pattern_naming_expr
-  | IntroAction of 'constr intro_pattern_action_expr
-and 'constr intro_pattern_action_expr =
-  | IntroWildcard
-  | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
-  | IntroInjection of ('constr intro_pattern_expr) CAst.t list
-  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
-  | IntroRewrite of bool
-and 'constr or_and_intro_pattern_expr =
-  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list
-  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list
-
-(** Bindings *)
-
-type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
-
-type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
-
-type 'a bindings =
-  | ImplicitBindings of 'a list
-  | ExplicitBindings of 'a explicit_bindings
-  | NoBindings
-
-type 'a with_bindings = 'a * 'a bindings
-
-(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
-   in the environment by the effective calls to Intro, Inversion, etc 
-   The [constr_expr] field is [None] in TacDef though *)
-type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
-type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern
-
-type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
-
-type delayed_open_constr = EConstr.constr delayed_open
-type delayed_open_constr_with_bindings = EConstr.constr with_bindings 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 = Namegen.intro_pattern_naming_expr CAst.t