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/language/core/definitions.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/language/core/definitions.rst')
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 79489c85f6..57771c9036 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,7 +90,7 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), + :attr:`program` (see :ref:`program_definition`), :attr:`canonical` and :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. |