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.

4 files changed, 32 insertions, 0 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index ead4e39692..20ee7aa4fb 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -82,3 +82,13 @@ let () =
   register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
   register_name0 wit_bindings "Constrarg.wit_bindings";
   register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings";
+  ()
+
+(** 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
index 5c26af3c2a..1197b85a25 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -72,3 +72,15 @@ val wit_red_expr :
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) 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/stdarg.ml b/interp/stdarg.ml
index 56b995e537..e497c996f7 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -28,3 +28,8 @@ let () = register_name0 wit_bool "Stdarg.wit_bool"
 let () = register_name0 wit_int "Stdarg.wit_int"
 let () = register_name0 wit_string "Stdarg.wit_string"
 let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident"
+
+(** Aliases for compatibility *)
+
+let wit_integer = wit_int
+let wit_preident = wit_pre_ident
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index d8904dab87..e1f648d7fc 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type
 val wit_string : string uniform_genarg_type
 
 val wit_pre_ident : string uniform_genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_integer : int uniform_genarg_type
+val wit_preident : string uniform_genarg_type