diff options
| author | Maxime Dénès | 2019-05-16 18:20:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-06-06 08:54:39 +0200 |
| commit | fb30e8880a3027ef1c957df668a906d723e8a8a0 (patch) | |
| tree | ad2825c374340dfa0bb4c8785034e689c0311d61 /doc/changelog | |
| parent | c0a695e89b0562eb6450c04ddba5e6e0414e5fd8 (diff) | |
`deprecated` attribute support for notations and syntactic definitions
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/03-notations/10180-deprecate-notations.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst new file mode 100644 index 0000000000..050aa105d8 --- /dev/null +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -0,0 +1,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. |