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.

12 files changed, 10 insertions, 14 deletions

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