Cutting the dependency of Genarg in constr_expr, glob_constr

related types. This will ultimately allow putting genargs into
these ASTs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 11 insertions, 7 deletions

diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 00f0cd715..ba35433f1 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -20,8 +20,8 @@ val hintbases : hint_db_name list option Pcoq.Gram.entry
 val wit_hintbases : hint_db_name list option Genarg.uniform_genarg_type
 
 val wit_auto_using :
-  (Genarg.open_constr_expr list,
-  Genarg.open_glob_constr list, Evd.open_constr list)
+  (Tacexpr.open_constr_expr list,
+  Tacexpr.open_glob_constr list, Evd.open_constr list)
     Genarg.genarg_type
 
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index cd4d777d6..1367f7032 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -26,7 +26,7 @@ val occurrences_of : int list -> Locus.occurrences
 
 val wit_glob :
   (constr_expr,
-  Genarg.glob_constr_and_expr,
+  Tacexpr.glob_constr_and_expr,
   Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
 val glob : constr_expr Pcoq.Gram.entry
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index e2dff62f8..5d31f24bc 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -214,7 +214,7 @@ type hypinfo = {
   l2r : bool;
   c1 : constr;
   c2 : constr;
-  c  : (Tacinterp.interp_sign * Genarg.glob_constr_and_expr with_bindings) option;
+  c  : (Tacinterp.interp_sign * Tacexpr.glob_constr_and_expr with_bindings) option;
   abs : (constr * types) option;
   flags : Unification.unify_flags;
 }
@@ -1372,8 +1372,8 @@ let interp_glob_constr_list env sigma =
 (* Syntax for rewriting with strategies *)
 
 type constr_expr_with_bindings = constr_expr with_bindings
-type glob_constr_with_bindings = glob_constr_and_expr with_bindings
-type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
+type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
+type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings
 
 let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge)))
 let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge))
@@ -1461,7 +1461,7 @@ let rec strategy_of_ast = function
 
 
 type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
-type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
+type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
 
 let interp_strategy ist gl s = 
   let sigma = project gl in
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index e530a5fbd..0d1a48f50 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -15,6 +15,7 @@ open Pattern
 open Misctypes
 open Genarg
 open Stdarg
+open Constrarg
 
 exception CannotCoerceTo of string
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 456779732..d085704bb 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -25,6 +25,7 @@ open Constrexpr_ops
 open Termops
 open Tacexpr
 open Genarg
+open Constrarg
 open Mod_subst
 open Extrawit
 open Misctypes
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 06a3ad260..a13a8faf2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -34,6 +34,7 @@ open Tacexpr
 open Hiddentac
 open Genarg
 open Stdarg
+open Constrarg
 open Printer
 open Pretyping
 open Extrawit
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index ba80d6d6c..f1ada9364 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -10,6 +10,7 @@ open Util
 open Tacexpr
 open Mod_subst
 open Genarg
+open Constrarg
 open Misctypes
 open Globnames
 open Term