diff options
| author | Hugo Herbelin | 2020-03-17 10:37:30 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-22 13:28:40 +0100 |
| commit | 83e22b5abc05902d1468d1cf033251dae46b69bc (patch) | |
| tree | 561e9f5bcdbf6d76bbf7b7cbe002aa6773cdca25 /doc | |
| parent | 9c841105fe2b51305abcba7bd8a574705dbd1adf (diff) | |
Renaming "ident" into "name" in grammar entries, to prevent confusions.
We use a deprecation phase where:
- "ident" means "name" (as it used to mean), except in custom coercion
entries where it already meant "ident".
- "ident" will be made again available (outside situation of
coercions) to mean "ident" at the end of deprecation phase.
Also renaming "as ident" into "as name".
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst new file mode 100644 index 0000000000..8d681361e8 --- /dev/null +++ b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst @@ -0,0 +1,13 @@ +- **Changed:** + In notations (except in custom entries), the misleading :n:`@syntax_modifier` + :n:`@ident ident` (which accepted either an identifier or + a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If + the intent was really to only parse identifiers, this will + eventually become possible, but only as of Coq 8.15. + In custom entries, the meaning of :n:`@ident ident` is silently changed + from parsing identifiers or :g:`_` to parsing only identifiers + without warning, but this presumably affects only rare, recent and + relatively experimental code + (`#11841 <https://github.com/coq/coq/pull/11841>`_, + fixes `#9514 <https://github.com/coq/coq/pull/9514>`_, + by Hugo Herbelin). |