Merging Stdarg and Constrarg.

There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.

37 files changed, 147 insertions, 198 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 00078c69f..2792e5756 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -23,6 +23,8 @@ The following type aliases where removed
 
   Context.section_context    ... it was just an alias for "Context.Named.t" which is still available
 
+The module Constrarg was merged into Stdarg.
+
 ** Ltac API **
 
 Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e09477014..f99132a67 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -501,7 +501,7 @@ END
 
 open Pcoq
 open Genarg
-open Constrarg
+open Stdarg
 open Egramml
 
 let _ =
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
deleted file mode 100644
index b8baa6401..000000000
--- a/interp/constrarg.ml
+++ /dev/null
@@ -1,66 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Loc
-open Misctypes
-open Tactypes
-open Genarg
-open Geninterp
-
-let make0 ?dyn name =
-  let wit = Genarg.make0 name in
-  let () = Geninterp.register_val0 wit dyn in
-  wit
-
-(** 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 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, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
-  make0 "intropattern"
-
-let wit_ident =
-  make0 "ident"
-
-let wit_var =
-  make0 ~dyn:(val_tag (topwit wit_ident)) "var"
-
-let wit_ref = make0 "ref"
-
-let wit_quant_hyp = make0 "quant_hyp"
-
-let wit_constr =
-  make0 "constr"
-
-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_bindings = make0 "bindings"
-
-let wit_red_expr = make0 "redexpr"
-
-let wit_clause_dft_concl  =
-  make0 "clause_dft_concl"
-
-(** Aliases *)
-
-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/constrarg.mli b/interp/constrarg.mli
deleted file mode 100644
index 4b542675b..000000000
--- a/interp/constrarg.mli
+++ /dev/null
@@ -1,75 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \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 Names
-open Term
-open Libnames
-open Globnames
-open Genredexpr
-open Pattern
-open Constrexpr
-open Misctypes
-open Tactypes
-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, int or_var, int) 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
-
-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_constr : (constr_expr, glob_constr_and_expr, 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, 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_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,
-  (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
-
-(** Aliases for compatibility *)
-
-val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
-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, 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,
-  (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/interp.mllib b/interp/interp.mllib
index 96b52959a..607af82a0 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,5 +1,4 @@
 Stdarg
-Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 2a7d52e3a..341ff5662 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
+open Misctypes
+open Tactypes
 open Genarg
 open Geninterp
 
@@ -29,7 +32,49 @@ let wit_string : string uniform_genarg_type =
 let wit_pre_ident : string uniform_genarg_type =
   make0 ~dyn:(val_tag (topwit wit_string)) "preident"
 
+let loc_of_or_by_notation f = function
+  | AN c -> f c
+  | ByNotation (loc,s,_) -> loc
+
+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"
+
+let wit_var =
+  make0 ~dyn:(val_tag (topwit wit_ident)) "var"
+
+let wit_ref = make0 "ref"
+
+let wit_quant_hyp = make0 "quant_hyp"
+
+let wit_constr =
+  make0 "constr"
+
+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_bindings = make0 "bindings"
+
+let wit_red_expr = make0 "redexpr"
+
+let wit_clause_dft_concl  =
+  make0 "clause_dft_concl"
+
 (** Aliases for compatibility *)
 
 let wit_integer = wit_int
 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 e1f648d7f..af3a73462 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -8,8 +8,21 @@
 
 (** Basic generic arguments. *)
 
+open Loc
+open Names
+open Term
+open Libnames
+open Globnames
+open Genredexpr
+open Pattern
+open Constrexpr
+open Misctypes
+open Tactypes
 open Genarg
 
+(** FIXME: nothing to do there. *)
+val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
+
 val wit_unit : unit uniform_genarg_type
 
 val wit_bool : bool uniform_genarg_type
@@ -20,7 +33,54 @@ val wit_string : string uniform_genarg_type
 
 val wit_pre_ident : string uniform_genarg_type
 
+(** {5 Additional generic arguments} *)
+
+val wit_int_or_var : (int or_var, int or_var, int) 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
+
+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_constr : (constr_expr, glob_constr_and_expr, 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, 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_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,
+  (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
+
 (** Aliases for compatibility *)
 
 val wit_integer : int uniform_genarg_type
 val wit_preident : string uniform_genarg_type
+val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
+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, 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,
+  (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/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index de4d589ee..b6d731f9f 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -13,7 +13,7 @@ open Names
 open Locus
 open Misctypes
 open Genredexpr
-open Constrarg
+open Stdarg
 open Extraargs
 
 open Sigma.Notations
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 1176772cd..8a316419e 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -11,7 +11,6 @@
 open Pp
 open Genarg
 open Stdarg
-open Constrarg
 open Tacarg
 open Pcoq.Prim
 open Pcoq.Constr
@@ -32,12 +31,12 @@ let create_generic_quotation name e wit =
 let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
 let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
 
-let () = create_generic_quotation "ident" Pcoq.Prim.ident Constrarg.wit_ident
-let () = create_generic_quotation "reference" Pcoq.Prim.reference Constrarg.wit_ref
-let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr
-let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr
-let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Constrarg.wit_intro_pattern
-let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr
+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 "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
   Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5)
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index de701bb23..cadd7ef2c 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -11,7 +11,6 @@
 open Pp
 open Genarg
 open Stdarg
-open Constrarg
 open Tacarg
 open Extraargs
 open Pcoq.Prim
@@ -28,7 +27,6 @@ open Equality
 open Misctypes
 open Sigma.Notations
 open Proofview.Notations
-open Constrarg
 
 DECLARE PLUGIN "extratactics"
 
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 2165e826e..82ba63871 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -11,7 +11,6 @@
 open Pp
 open Genarg
 open Stdarg
-open Constrarg
 open Pcoq.Prim
 open Pcoq.Constr
 open Pltac
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index b662057ba..d551b7315 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -12,7 +12,6 @@ open Misctypes
 open Class_tactics
 open Pltac
 open Stdarg
-open Constrarg
 open Tacarg
 
 DECLARE PLUGIN "g_class"
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index cce068910..d128b4d08 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -32,8 +32,8 @@ 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 Constrarg.wit_intro_pattern) pat
-let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
+let genarg_of_ipattern pat = in_gen (rawwit Stdarg.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
 
 let reference_to_id = function
@@ -353,7 +353,7 @@ GEXTEND Gram
   ;
   END
 
-open Constrarg
+open Stdarg
 open Tacarg
 open Vernacexpr
 open Vernac_classifier
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index fd531ca69..d286a5870 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -17,7 +17,6 @@ open Libnames
 open Constrexpr
 open Constrexpr_ops
 open Stdarg
-open Constrarg
 open Tacarg
 open Extraargs
 
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index cdcbfdb7c..3168898a3 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -21,7 +21,6 @@ open Tacmach
 open Tacticals
 open Rewrite
 open Stdarg
-open Constrarg
 open Pcoq.Vernac_
 open Pcoq.Prim
 open Pcoq.Constr
diff --git a/ltac/pltac.ml b/ltac/pltac.ml
index 94bf32d1d..fb5204d89 100644
--- a/ltac/pltac.ml
+++ b/ltac/pltac.ml
@@ -49,7 +49,6 @@ let tactic_eoi = eoi_entry tactic
 
 let () =
   let open Stdarg in
-  let open Constrarg in
   let open Tacarg in
   register_grammar wit_int_or_var (int_or_var);
   register_grammar wit_intro_pattern (simple_intropattern);
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index f738d2150..5f2617e44 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -15,7 +15,7 @@ open Constrexpr
 open Tacexpr
 open Genarg
 open Geninterp
-open Constrarg
+open Stdarg
 open Tacarg
 open Libnames
 open Ppextend
@@ -1261,53 +1261,53 @@ let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
   let pr_string s = str "\"" ++ str s ++ str "\"" in
-  Genprint.register_print0 Constrarg.wit_int_or_var
+  Genprint.register_print0 wit_int_or_var
     (pr_or_var int) (pr_or_var int) int;
-  Genprint.register_print0 Constrarg.wit_ref
+  Genprint.register_print0 wit_ref
     pr_reference (pr_or_var (pr_located pr_global)) pr_global;
-  Genprint.register_print0 Constrarg.wit_ident
+  Genprint.register_print0 wit_ident
     pr_id pr_id pr_id;
-  Genprint.register_print0 Constrarg.wit_var
+  Genprint.register_print0 wit_var
     (pr_located pr_id) (pr_located pr_id) pr_id;
   Genprint.register_print0
-    Constrarg.wit_intro_pattern
+    wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
     (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
   Genprint.register_print0
-    Constrarg.wit_clause_dft_concl
+    wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
     (pr_clauses (Some true) pr_lident)
     (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
   ;
   Genprint.register_print0
-    Constrarg.wit_constr
+    wit_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
     Printer.pr_constr
   ;
   Genprint.register_print0
-    Constrarg.wit_uconstr
+    wit_uconstr
     Ppconstr.pr_constr_expr
     (fun (c,_) -> Printer.pr_glob_constr c)
     Printer.pr_closed_glob
   ;
   Genprint.register_print0
-    Constrarg.wit_open_constr
+    wit_open_constr
     Ppconstr.pr_constr_expr
     (fun (c, _) -> Printer.pr_glob_constr c)
     Printer.pr_constr
   ;
-  Genprint.register_print0 Constrarg.wit_red_expr
+  Genprint.register_print0 wit_red_expr
     (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
     (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
     (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
-  Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
-  Genprint.register_print0 Constrarg.wit_bindings
+  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+  Genprint.register_print0 wit_bindings
     (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
     (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
-  Genprint.register_print0 Constrarg.wit_constr_with_bindings
+  Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
     (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it)));
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
index 46469df6a..2af872daf 100644
--- a/ltac/taccoerce.ml
+++ b/ltac/taccoerce.ml
@@ -13,7 +13,6 @@ open Pattern
 open Misctypes
 open Genarg
 open Stdarg
-open Constrarg
 open Geninterp
 
 exception CannotCoerceTo of string
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index b0b4dc357..763e0dc22 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -23,7 +23,7 @@ open Constrexpr
 open Termops
 open Tacexpr
 open Genarg
-open Constrarg
+open Stdarg
 open Tacarg
 open Misctypes
 open Locus
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index a65e58ddb..92a403c58 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -31,7 +31,6 @@ open Tacexpr
 open Genarg
 open Geninterp
 open Stdarg
-open Constrarg
 open Tacarg
 open Printer
 open Pretyping
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index e0fdc4e5a..55de58361 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -10,7 +10,7 @@ open Util
 open Tacexpr
 open Mod_subst
 open Genarg
-open Constrarg
+open Stdarg
 open Tacarg
 open Misctypes
 open Globnames
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index e3a66dc11..ef707790c 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -458,7 +458,6 @@ let with_grammar_rule_protection f x =
 
 let () =
   let open Stdarg in
-  let open Constrarg in
   Grammar.register0 wit_int (Prim.integer);
   Grammar.register0 wit_string (Prim.string);
   Grammar.register0 wit_pre_ident (Prim.preident);
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 52a135119..6f6811334 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -10,7 +10,6 @@
 
 open Cctac
 open Stdarg
-open Constrarg
 
 DECLARE PLUGIN "cc_plugin"
 
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index d4dc7e0ee..deadb3b4d 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Constrarg
+open Stdarg
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 19fda4aea..e1d6bb4a8 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -14,7 +14,6 @@ DECLARE PLUGIN "extraction_plugin"
 
 open Genarg
 open Stdarg
-open Constrarg
 open Pcoq.Prim
 open Pp
 open Names
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 487162687..344a04a6a 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,9 +15,8 @@ open Goptions
 open Tacticals
 open Tacinterp
 open Libnames
-open Constrarg
-open Tacarg
 open Stdarg
+open Tacarg
 open Pcoq.Prim
 
 DECLARE PLUGIN "ground_plugin"
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6368c2536..6603a95a8 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -14,7 +14,7 @@ open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
-open Constrarg
+open Stdarg
 open Misctypes
 open Pcoq.Prim
 open Pcoq.Constr
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index aadcf060e..79020ed03 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,7 +16,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open Constrarg
+open Stdarg
 open Tacarg
 
 DECLARE PLUGIN "micromega_plugin"
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 5647fbf9f..27115abec 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -19,7 +19,7 @@ DECLARE PLUGIN "omega_plugin"
 
 open Names
 open Coq_omega
-open Constrarg
+open Stdarg
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index ebd19428f..e7e6ecef9 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,7 +13,7 @@ open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
-open Constrarg
+open Stdarg
 open Tacarg
 
 DECLARE PLUGIN "quote_plugin"
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 830dc54dd..2f38688d1 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -12,7 +12,7 @@ DECLARE PLUGIN "romega_plugin"
 
 open Names
 open Refl_omega
-open Constrarg
+open Stdarg
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 13e225404..0987c44ae 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -15,7 +15,6 @@ open Printer
 open Newring_ast
 open Newring
 open Stdarg
-open Constrarg
 open Tacarg
 open Pcoq.Constr
 open Pltac
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a5e2211d8..657efe175 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -124,8 +124,8 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
   TacML(Loc.ghost,tacname,
-  [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
-   TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)]))
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
+   TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 099918c35..bedf925e8 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -19,7 +19,7 @@ open Names
 open Pp
 open Pcoq
 open Genarg
-open Constrarg
+open Stdarg
 open Tacarg
 open Term
 open Vars
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index 24b4c1515..726c0ffcf 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -9,7 +9,6 @@
 open Ppextend
 open Constrexpr
 open Vernacexpr
-open Tacexpr
 open Genarg
 
 type t =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b85328402..1cb71da69 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -145,7 +145,7 @@ let conclPattern concl pat tac =
        constr_bindings env sigma >>= fun constr_bindings ->
      let open Genarg in
      let open Geninterp in
-     let inj c = match val_tag (topwit Constrarg.wit_constr) with
+     let inj c = match val_tag (topwit Stdarg.wit_constr) with
      | Val.Base tag -> Val.Dyn (tag, c)
      | _ -> assert false
      in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 14d9a55c6..aa1999cf1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -408,13 +408,13 @@ let print_located_library r =
 
 let smart_global r =
   let gr = Smartlocate.smart_global r in
-    Dumpglob.add_glob (Constrarg.loc_of_or_by_notation loc_of_reference r) gr;
+    Dumpglob.add_glob (Stdarg.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 (Constrarg.loc_of_or_by_notation loc_of_reference r) gr
+    Dumpglob.add_glob (Stdarg.loc_of_or_by_notation loc_of_reference r) gr
   with e when CErrors.noncritical e -> ()
 (**********)
 (* Syntax *)