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.

1 files changed, 9 insertions, 0 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 0581a5f850..1f5ba7862f 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -66,6 +66,15 @@
     Context.Named.t = LocalAssum of Names.Id.t * Constr.t
 	            | LocalDef of Names.Id.t * Constr.t * Constr.t
 
+- The various EXTEND macros do not handle specially the Coq-defined entries
+  anymore. Instead, they just output a name that have to exist in the scope
+  of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for
+  variables "$name" of type Gram.entry, while the parsing rules of
+  (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will
+  look for variables "wit_$name" of type Genarg.genarg_type. The small DSL
+  for constructing compound entries still works over this scheme. Note that in
+  the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
+  in the parsing rules, so beware of recursive calls.
 
 =========================================
 = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =