blob: a3c185d5f1282d4b23ab1ad2827cf58ee8b7c4cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
- **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).
|
