blob: bce5db5865ff991f26e6a036e259d6a5579e6134 (
plain)
1
2
3
4
5
6
|
- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated`
attribute. 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).
|
