diff options
Diffstat (limited to 'doc/changelog/03-notations/10180-deprecate-notations.rst')
| -rw-r--r-- | doc/changelog/03-notations/10180-deprecate-notations.rst | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst deleted file mode 100644 index a3c185d5f1..0000000000 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **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 - (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). |