Rationalizing the use of the various EXTEND macros.

Those macros used to handle in a special way the grammar entries and generic
arguments known statically from Coq, i.e. defined before Pcoq. This was hardly
predictible and very implementation-dependent.

We made the EXTEND macros much more light-weight by treating in a uniform way
all entries and arguments. Now, they are all produced by outputing the name
as-is for entries and as "wit_$name" for genargs, thus letting the scope
of the ML code decide which entrie is going to be taken. This is documented
in the dev/ changelog.

This also allows to get rid of a lot of dependencies in the grammar preprocessor,
reducing it to a small functional shell. It is still depending on Compat, but it
is most probably possible to reduce the code size even more.

11 files changed, 40 insertions, 3 deletions

diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 5dbc340caa..9a53e2e16a 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -9,6 +9,10 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Cctac
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 
 DECLARE PLUGIN "cc_plugin"
 
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 2d096a1081..2afbaca2c8 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -95,7 +95,7 @@ let proof_mode : vernac_expr Gram.entry =
   Gram.entry_create "vernac:proof_command"
 (* Auxiliary grammar entry. *)
 let proof_instr : raw_proof_instr Gram.entry =
-  Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr)
+  Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
 
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 18570a6846..35a5a7616c 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index aec9586895..7bd07f6255 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -11,6 +11,10 @@
 (* ML names *)
 
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 open Pp
 open Names
 open Nameops
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 3e8be36993..587d10d1cc 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,6 +15,10 @@ open Goptions
 open Tacticals
 open Tacinterp
 open Libnames
+open Constrarg
+open Stdarg
+open Pcoq.Prim
+open Pcoq.Tactic
 
 DECLARE PLUGIN "ground_plugin"
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 61ada5cc8c..e93c395e3d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -16,8 +16,12 @@ open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
+open Constrarg
 open Tacticals
 open Misctypes
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "recdef_plugin"
 
@@ -90,7 +94,7 @@ let out_disjunctive = function
   | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
   | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected."
 
-ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat
+ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
 |   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ]
 | []  ->[ None ]
 END
@@ -149,7 +153,7 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar
   Genarg.create_arg "function_rec_definition_loc"
 
 let function_rec_definition_loc =
-  Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+  Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
 
 GEXTEND Gram
   GLOBAL: function_rec_definition_loc ;
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index bfc9c727d5..bca1c2febd 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -18,6 +18,10 @@
 
 open Errors
 open Misctypes
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Tactic
 
 DECLARE PLUGIN "micromega_plugin"
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 04c62eb487..b314e0d85f 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -19,6 +19,8 @@ DECLARE PLUGIN "omega_plugin"
 
 open Names
 open Coq_omega
+open Constrarg
+open Pcoq.Prim
 
 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 7a3d7936a6..a15b0eb05a 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,6 +13,10 @@ open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "quote_plugin"
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 6b2b2bbfaf..61efa9f545 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -12,6 +12,8 @@ DECLARE PLUGIN "romega_plugin"
 
 open Names
 open Refl_omega
+open Constrarg
+open Pcoq.Prim
 
 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 856ec0db5f..cd1d704dde 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -14,6 +14,11 @@ open Libnames
 open Printer
 open Newring_ast
 open Newring
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "newring_plugin"