Untangling Tacexpr from lower strata.

4 files changed, 16 insertions, 14 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index aaf33a956..b8baa6401 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -8,6 +8,7 @@
 
 open Loc
 open Misctypes
+open Tactypes
 open Genarg
 open Geninterp
 
@@ -26,7 +27,7 @@ let loc_of_or_by_notation f = function
 let wit_int_or_var =
   make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
 
-let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type =
+let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
   make0 "intropattern"
 
 let wit_ident =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 32f2dc6f3..4b542675b 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -18,6 +18,7 @@ open Genredexpr
 open Pattern
 open Constrexpr
 open Misctypes
+open Tactypes
 open Genarg
 
 (** FIXME: nothing to do there. *)
@@ -27,7 +28,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
 
 val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
-val wit_intro_pattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type
+val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
 
 val wit_ident : Id.t uniform_genarg_type
 
@@ -37,26 +38,26 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
 
 val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
 
-val wit_constr : (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type
+val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
 
-val wit_uconstr : (constr_expr , Tacexpr.glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
+val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
 
 val wit_open_constr :
-  (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type
+  (constr_expr, glob_constr_and_expr, constr) genarg_type
 
 val wit_constr_with_bindings :
   (constr_expr with_bindings,
-  Tacexpr.glob_constr_and_expr with_bindings,
-  constr with_bindings Pretyping.delayed_open) genarg_type
+  glob_constr_and_expr with_bindings,
+  constr with_bindings delayed_open) genarg_type
 
 val wit_bindings :
   (constr_expr bindings,
-  Tacexpr.glob_constr_and_expr bindings,
-  constr bindings Pretyping.delayed_open) genarg_type
+  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,
-  (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
@@ -67,8 +68,8 @@ val wit_reference : (reference, global_reference located or_var, global_referenc
 val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
 val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located 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 located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
 val wit_redexpr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
-  (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 693101a47..be7abfa99 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -16,7 +16,7 @@ type glob_sign = {
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
-type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 module InternObj =
 struct
diff --git a/interp/genintern.mli b/interp/genintern.mli
index aabb85e00..4b0354be3 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -34,7 +34,7 @@ val generic_substitute : glob_generic_argument subst_fun
 
 (** {5 Notation functions} *)
 
-type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun