diff options
| author | Emilio Jesus Gallego Arias | 2020-11-12 20:21:36 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-18 16:24:28 +0100 |
| commit | c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b (patch) | |
| tree | 88036bf297a2b4572e6822f584fb2dbc28826385 /doc/sphinx/changes.rst | |
| parent | e0380f347d2ebf61b81760a365eea8c84ad3ada4 (diff) | |
[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.
We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).
We update the documentation, test-suite, and changelog.
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index de5dbe79cc..4d59fc0513 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -533,8 +533,8 @@ Flags, options and attributes - **Removed:** Unqualified ``polymorphic``, ``monomorphic``, ``template``, ``notemplate`` attributes (they were deprecated since Coq 8.10). - Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)` and :attr:`universes(notemplate)` instead + Use :attr:`universes(polymorphic)`, ``universes(monomorphic)``, + :attr:`universes(template)` and ``universes(notemplate)`` instead (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). - **Deprecated:** :flag:`Hide Obligations` flag @@ -545,7 +545,7 @@ Flags, options and attributes <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). - **Added:** New attributes supported when defining an inductive type - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`universes(cumulative)`, ``universes(noncumulative)`` and :attr:`private(matching)`, which correspond to legacy attributes ``Cumulative``, ``NonCumulative``, and the previously undocumented ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by |