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.

14 files changed, 26 insertions, 36 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index de4d589eee..b6d731f9f0 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 1176772cdc..8a316419e8 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 de701bb239..cadd7ef2c9 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 2165e826ed..82ba63871e 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 b662057ba3..d551b7315a 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 cce0689107..d128b4d086 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 fd531ca691..d286a58708 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 cdcbfdb7cb..3168898a37 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 94bf32d1d5..fb5204d891 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 f738d21502..5f2617e44d 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 46469df6a1..2af872daf6 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 b0b4dc3579..763e0dc22e 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 a65e58ddb0..92a403c585 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 e0fdc4e5a1..55de583613 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