diff options
| author | Théo Zimmermann | 2019-10-22 11:20:07 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-28 10:04:32 +0100 |
| commit | fbdde37d9d7d2fce7fe9b7035ad0e8efa7799dff (patch) | |
| tree | a6d68fd1a86a6e6adbae7d6dcf0e76f09425efe5 /doc/changelog/03-notations | |
| parent | 570018fe2c37eee1f87d509037162768bffe6366 (diff) | |
[changelog] Add types to changelog entries.
Types of changes are defined in the list defined by Keep a Changelog
1.0.0 (https://keepachangelog.com/en/1.0.0/):
- Added
- Changed
- Deprecated
- Fixed
- Removed
We exclude the type Security for now, even for soundness fixes,
because the process of handling security vulnerabilities is different
from anything we follow right now.
Diffstat (limited to 'doc/changelog/03-notations')
3 files changed, 11 insertions, 4 deletions
diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst index abc5a516ae..ed95a6eb4f 100644 --- a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst +++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst @@ -1,4 +1,5 @@ -- Numeral Notations now support sorts in the input to printing +- **Added:** + Numeral Notations now support sorts in the input to printing functions (e.g., numeral notations can be defined for terms containing things like `@cons Set nat nil`). (`#9883 <https://github.com/coq/coq/pull/9883>`_, by Jason Gross). diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst index bce5db5865..a3c185d5f1 100644 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -1,5 +1,10 @@ -- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` - attribute. The former `compat` annotation for notations is +- **Added:** + The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` + attribute + (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). + +- **Deprecated:** + The former `compat` annotation for notations is deprecated, and its semantics changed. It is now made equivalent to using a `deprecated` attribute, and is no longer connected with the `-compat` command-line flag diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst index 327a39bdb6..5dc0215225 100644 --- a/doc/changelog/03-notations/10963-simplify-parser.rst +++ b/doc/changelog/03-notations/10963-simplify-parser.rst @@ -1,4 +1,5 @@ -- A simplification of parsing rules could cause a slight change of +- **Changed:** + A simplification of parsing rules could cause a slight change of parsing precedences for the very rare users who defined notations with `constr` at level strictly between 100 and 200 and used these notations on the right-hand side of a cast operator (`:`, `:>`, |