[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.

8 files changed, 39 insertions, 5 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 1070b30a1..8f59559eb 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -15,6 +15,7 @@ open Tactypes
 open Genredexpr
 open Stdarg
 open Extraargs
+open Tacarg
 open Names
 open Logic
 
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 4e7c8b754..ddc157cac 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -35,7 +35,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
 let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
 let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
 let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr
-let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern
+let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern
 let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index de9ff2875..c39192d46 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -36,7 +36,7 @@ let arg_of_expr = function
 
 let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
 let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
-let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat
+let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat
 let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
 let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 6eb482b1c..8a25d4851 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -19,6 +19,14 @@ let make0 ?dyn name =
   let () = Geninterp.register_val0 wit dyn in
   wit
 
+let wit_intro_pattern = make0 "intropattern"
+let wit_quant_hyp = make0 "quant_hyp"
+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_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
   make0 "tactic"
 
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index 1abe7cd6f..bdb0be03c 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -9,9 +9,33 @@
 (************************************************************************)
 
 open Genarg
-open Tacexpr
+open EConstr
 open Constrexpr
 open Tactypes
+open Tacexpr
+
+(** Tactic related witnesses, could also live in tactics/ if other users *)
+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_quant_hyp : quantified_hypothesis uniform_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_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
 
 (** Generic arguments based on Ltac. *)
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 27acbb629..6bfa07ee9 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -17,6 +17,7 @@ open Namegen
 open Tactypes
 open Genarg
 open Stdarg
+open Tacarg
 open Geninterp
 open Pp
 
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 289434d8a..f4dd85bc2 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -118,7 +118,7 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+type glob_constr_and_expr = Genintern.glob_constr_and_expr
 
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 42f6883b4..be07654ef 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -118,7 +118,7 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+type glob_constr_and_expr = Genintern.glob_constr_and_expr
 
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr