blob: 050aa105d86e213b446b0026936d46f117f8119d (
plain)
1
2
3
4
5
6
|
- The `Notation` and `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.
|
