diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-18 01:36:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-18 01:37:26 +0100 |
| commit | f8f1f9d38bf2d35b0dc69fbf2e8ebbfc04b1a82d (patch) | |
| tree | 9e4d24d9bf13dbdeaf53dcfc025604f09890b078 | |
| parent | 1730369cd4f7b62a076c93b2a0ece190ee08f7eb (diff) | |
Documenting the change of EXTEND macros.
| -rw-r--r-- | dev/doc/changes.txt | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 0581a5f85..1f5ba7862 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 = |