diff options
| author | Emilio Jesus Gallego Arias | 2019-11-29 14:57:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-29 14:57:09 +0100 |
| commit | 18ad1b309bbdcf8aa4cc12b024b88007dfd9c14f (patch) | |
| tree | f75031945fede844f5b80d80d2ee08ee336953b6 /doc/changelog/03-notations | |
| parent | 09eea7a192744ad171c83621561c8edf12b31578 (diff) | |
| parent | ae219c035bfc64bf817cd1cbedafb75dfdb8e893 (diff) | |
Merge PR #10931: Add types of changes to changelog entries.
Ack-by: SkySkimmer
Reviewed-by: ejgallego
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 (`:`, `:>`, |