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

24 files changed, 200 insertions, 155 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index c16b4abba..80eaa6b85 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -126,6 +126,7 @@ Ppextend
 Pputils
 Genarg
 Stdarg
+Constrarg
 Constrexpr_ops
 Notation_ops
 Topconstr
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f59c300a9..a9b942e7b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -409,6 +409,7 @@ END
 
 open Pcoq
 open Genarg
+open Constrarg
 open Egramml
 
 let _ =
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 6fde4fafe..dffca2c62 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -33,20 +33,20 @@ let mk_extraarg s =
     qualified_name ("Extrawit.wit_" ^ s)
 
 let rec make_wit loc = function
-  | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >>
-  | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >>
-  | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >>
-  | VarArgType -> <:expr< Genarg.wit_var >>
-  | RefArgType -> <:expr< Genarg.wit_ref >>
-  | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
-  | GenArgType -> <:expr< Genarg.wit_genarg >>
-  | SortArgType -> <:expr< Genarg.wit_sort >>
-  | ConstrArgType -> <:expr< Genarg.wit_constr >>
-  | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
-  | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
-  | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
-  | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
-  | BindingsArgType -> <:expr< Genarg.wit_bindings >>
+  | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
+  | IntroPatternArgType -> <:expr< Constrarg.wit_intro_pattern >>
+  | IdentArgType b -> <:expr< Constrarg.wit_ident_gen $mlexpr_of_bool b$ >>
+  | VarArgType -> <:expr< Constrarg.wit_var >>
+  | RefArgType -> <:expr< Constrarg.wit_ref >>
+  | QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >>
+  | GenArgType -> <:expr< Constrarg.wit_genarg >>
+  | SortArgType -> <:expr< Constrarg.wit_sort >>
+  | ConstrArgType -> <:expr< Constrarg.wit_constr >>
+  | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
+  | RedExprArgType -> <:expr< Constrarg.wit_red_expr >>
+  | OpenConstrArgType b -> <:expr< Constrarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
+  | ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >>
+  | BindingsArgType -> <:expr< Constrarg.wit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
   | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index a97b8a2a6..f361bee49 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -28,6 +28,7 @@ Names
 Libnames
 Genarg
 Stdarg
+Constrarg
 Tok
 Lexer
 Extrawit
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
new file mode 100644
index 000000000..540bca62e
--- /dev/null
+++ b/interp/constrarg.ml
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Loc
+open Pp
+open Names
+open Term
+open Libnames
+open Globnames
+open Glob_term
+open Genredexpr
+open Pattern
+open Constrexpr
+open Term
+open Misctypes
+open Genarg
+
+(** This is a hack for now, to break the dependency of Genarg on constr-related
+    types. We should use dedicated functions someday. *)
+
+let loc_of_or_by_notation f = function
+  | AN c -> f c
+  | ByNotation (loc,s,_) -> loc
+
+let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
+  Obj.magic t
+
+let wit_int_or_var = unsafe_of_type IntOrVarArgType
+
+let wit_intro_pattern = unsafe_of_type IntroPatternArgType
+
+let wit_ident_gen b = unsafe_of_type (IdentArgType b)
+
+let wit_ident = wit_ident_gen true
+
+let wit_pattern_ident = wit_ident_gen false
+
+let wit_var = unsafe_of_type VarArgType
+
+let wit_ref = unsafe_of_type RefArgType
+
+let wit_quant_hyp = unsafe_of_type QuantHypArgType
+
+let wit_genarg = unsafe_of_type GenArgType
+
+let wit_sort = unsafe_of_type SortArgType
+
+let wit_constr = unsafe_of_type ConstrArgType
+
+let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
+
+let wit_open_constr_gen b = unsafe_of_type (OpenConstrArgType b)
+
+let wit_open_constr = wit_open_constr_gen false
+
+let wit_casted_open_constr = wit_open_constr_gen true
+
+let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
+
+let wit_bindings = unsafe_of_type BindingsArgType
+
+let wit_red_expr = unsafe_of_type RedExprArgType
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
new file mode 100644
index 000000000..548bd6690
--- /dev/null
+++ b/interp/constrarg.mli
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Generic arguments based on [constr]. We put them here to avoid a dependency
+    of Genarg in [constr]-related interfaces. *)
+
+open Loc
+open Pp
+open Names
+open Term
+open Libnames
+open Globnames
+open Glob_term
+open Genredexpr
+open Pattern
+open Constrexpr
+open Tacexpr
+open Term
+open Misctypes
+open Evd
+open Genarg
+
+(** FIXME: nothing to do there. *)
+val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
+
+(** {5 Additional generic arguments} *)
+
+val wit_int_or_var : int or_var uniform_genarg_type
+
+val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
+
+val wit_ident : Id.t uniform_genarg_type
+
+val wit_pattern_ident : Id.t uniform_genarg_type
+
+val wit_ident_gen : bool -> Id.t uniform_genarg_type
+
+val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
+
+val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
+
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+
+val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type
+
+val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
+
+val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
+
+val wit_constr_may_eval :
+  ((constr_expr,reference or_by_notation,constr_expr) may_eval,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
+  constr) genarg_type
+
+val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings sigma) genarg_type
+
+val wit_bindings :
+  (constr_expr bindings,
+  glob_constr_and_expr bindings,
+  constr bindings sigma) 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,
+  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 83038c8ba..c0526d508 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -9,9 +9,6 @@
 open Pp
 open Util
 open Names
-open Glob_term
-open Constrexpr
-open Misctypes
 
 type argument_type =
   (* Basic types *)
@@ -59,16 +56,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2
 | _ -> false
 
-let loc_of_or_by_notation f = function
-  | AN c -> f c
-  | ByNotation (loc,s,_) -> loc
-
-type glob_constr_and_expr = glob_constr * constr_expr option
-type open_constr_expr = unit * constr_expr
-type open_glob_constr = unit * glob_constr_and_expr
-
-type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern
-
 type ('raw, 'glob, 'top) genarg_type = argument_type
 
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
@@ -89,42 +76,6 @@ let rawwit t = t
 let glbwit t = t
 let topwit t = t
 
-let wit_int_or_var = IntOrVarArgType
-
-let wit_intro_pattern = IntroPatternArgType
-
-let wit_ident_gen b = IdentArgType b
-
-let wit_ident = wit_ident_gen true
-
-let wit_pattern_ident = wit_ident_gen false
-
-let wit_var = VarArgType
-
-let wit_ref = RefArgType
-
-let wit_quant_hyp = QuantHypArgType
-
-let wit_genarg = GenArgType
-
-let wit_sort = SortArgType
-
-let wit_constr = ConstrArgType
-
-let wit_constr_may_eval = ConstrMayEvalArgType
-
-let wit_open_constr_gen b = OpenConstrArgType b
-
-let wit_open_constr = wit_open_constr_gen false
-
-let wit_casted_open_constr = wit_open_constr_gen true
-
-let wit_constr_with_bindings = ConstrWithBindingsArgType
-
-let wit_bindings = BindingsArgType
-
-let wit_red_expr = RedExprArgType
-
 let wit_list0 t = List0ArgType t
 
 let wit_list1 t = List1ArgType t
diff --git a/interp/genarg.mli b/interp/genarg.mli
index bbd783047..629bd62a7 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -9,28 +9,6 @@
 open Loc
 open Pp
 open Names
-open Term
-open Libnames
-open Globnames
-open Glob_term
-open Genredexpr
-open Pattern
-open Constrexpr
-open Term
-open Misctypes
-
-(** FIXME: nothing to do there. *)
-val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
-
-(** 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_constr * constr_expr option
-
-type open_constr_expr = unit * constr_expr
-type open_glob_constr = unit * glob_constr_and_expr
-
-type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
 (** The route of a generic argument, from parsing to evaluation.
 In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
@@ -303,58 +281,6 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type
 
 (** {5 Basic generic type constructors} *)
 
-(** {6 Ground types} *)
-
-open Evd
-
-val wit_int_or_var : int or_var uniform_genarg_type
-
-val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
-
-val wit_ident : Id.t uniform_genarg_type
-
-val wit_pattern_ident : Id.t uniform_genarg_type
-
-val wit_ident_gen : bool -> Id.t uniform_genarg_type
-
-val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
-
-val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
-
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-
-val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type
-
-val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
-
-val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
-
-val wit_constr_may_eval :
-  ((constr_expr,reference or_by_notation,constr_expr) may_eval,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
-  constr) genarg_type
-
-val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_constr_with_bindings :
-  (constr_expr with_bindings,
-  glob_constr_and_expr with_bindings,
-  constr with_bindings sigma) genarg_type
-
-val wit_bindings :
-  (constr_expr bindings,
-  glob_constr_and_expr bindings,
-  constr bindings sigma) 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,
-  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-
 (** {6 Parameterized types} *)
 
 val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 86440bc29..77e2e5c00 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -17,3 +17,4 @@ Constrextern
 Coqlib
 Discharge
 Declare
+Constrarg
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index dbe888714..c253e888d 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -87,6 +87,18 @@ type ('a,'t) match_rule =
   | Pat of 'a match_context_hyps list * 'a match_pattern * 't
   | All of 't
 
+(** Composite types *)
+
+(** 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 open_constr_expr = unit * constr_expr
+type open_glob_constr = unit * glob_constr_and_expr
+
+type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
+
 (** Generic expressions for atomic tactics *)
 
 type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 06120a0a0..2769612d5 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -14,6 +14,7 @@ open Util
 open Extend
 open Genarg
 open Stdarg
+open Constrarg
 open Tacexpr
 open Extrawit
 
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 5b7f0b4c7..7548c338a 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -83,8 +83,8 @@ type raw_proof_instr =
      raw_tactic_expr) gen_proof_instr
 
 type glob_proof_instr =
-    ((Id.t*(Genarg.glob_constr_and_expr option)) Loc.located,
-     Genarg.glob_constr_and_expr,
+    ((Id.t*(Tacexpr.glob_constr_and_expr option)) Loc.located,
+     Tacexpr.glob_constr_and_expr,
      Constrexpr.cases_pattern_expr,
      Tacexpr.glob_tactic_expr) gen_proof_instr
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 8b90824fd..7ab9488de 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -82,7 +82,7 @@ let pr_intro_as_pat prc _ _ pat =
     | None -> mt ()
 
 
-ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat
+ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat
 |   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ]
 | []  ->[ None ]
 END
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 03d7c645e..d5c8094d4 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -122,15 +122,15 @@ END;;*)
 let closed_term_ast l =
   TacFun([Some(Id.of_string"t")],
   TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
-  [Genarg.in_gen Genarg.wit_constr (mkVar(Id.of_string"t"));
-   Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l])))
+  [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t"));
+   Genarg.in_gen (Genarg.wit_list1 Constrarg.wit_ref) l])))
 *)
 let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
   TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
-  [Genarg.in_gen (Genarg.glbwit Genarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
-   Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Genarg.wit_ref)) l])))
+  [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
+   Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Constrarg.wit_ref)) l])))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 432138916..2ff19c960 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -14,6 +14,7 @@ open Util
 open Constrexpr
 open Tacexpr
 open Genarg
+open Constrarg
 open Libnames
 open Ppextend
 open Misctypes
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index a9cd025a7..3b9858f16 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -22,7 +22,7 @@ val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t
 val match_pattern_printer :
   (env -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t
 val match_rule_printer :
-  ((Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
+  ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
 
 (** Debug information *)
 type debug_info =
@@ -41,7 +41,7 @@ val db_constr : debug_info -> env -> constr -> unit
 
 (** Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
+  debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :
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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 841919a29..526aa9230 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -419,13 +419,13 @@ let print_located_tactic r =
 
 let smart_global r =
   let gr = Smartlocate.smart_global r in
-    Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr;
+    Dumpglob.add_glob (Constrarg.loc_of_or_by_notation loc_of_reference r) gr;
     gr
 
 let dump_global r =
   try
     let gr = Smartlocate.smart_global r in
-    Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr
+    Dumpglob.add_glob (Constrarg.loc_of_or_by_notation loc_of_reference r) gr
   with e when Errors.noncritical e -> ()
 (**********)
 (* Syntax *)