From c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 12 Nov 2020 20:21:36 +0100
Subject: [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.
---
 .../13312-attributes+bool_single.rst                        | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/13312-attributes+bool_single.rst

(limited to 'doc/changelog')

diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
new file mode 100644
index 0000000000..fa046d968f
--- /dev/null
+++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
@@ -0,0 +1,13 @@
+- **Changed:**
+  Boolean attributes are now specified using key/value pairs, that is
+  to say ``attr={yes,no}``. If the value is missing, the default is
+  ``on``.  Old syntax is still supported, but produces the
+  ``deprecated-attribute-syntax`` warning.
+  Attributes deprecated are ``universes(monomorphic)``,
+  ``universes(notemplate)``, ``universes(noncumulative)``, which are
+  replaced by the corresponding ``universes(polymorphic=no)`` etc...
+  Attributes :attr:`program` and :attr:`canonical` are also affected,
+  with the syntax ``attr(false)`` being deprecated in favor of
+  ``attr=no``.
+  (`#13312 <https://github.com/coq/coq/pull/13312>`_,
+  by Emilio Jesus Gallego Arias).
-- 
cgit v1.2.3


From ca42305f1ed1699065cffdef7d96bf5fcc0069be Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 14 Nov 2020 18:44:57 +0100
Subject: Review commit: improving the doc of boolean attributes.

---
 .../13312-attributes+bool_single.rst               | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

(limited to 'doc/changelog')

diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
index fa046d968f..f069bc616b 100644
--- a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
+++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
@@ -1,13 +1,17 @@
 - **Changed:**
-  Boolean attributes are now specified using key/value pairs, that is
-  to say ``attr={yes,no}``. If the value is missing, the default is
-  ``on``.  Old syntax is still supported, but produces the
-  ``deprecated-attribute-syntax`` warning.
-  Attributes deprecated are ``universes(monomorphic)``,
-  ``universes(notemplate)``, ``universes(noncumulative)``, which are
-  replaced by the corresponding ``universes(polymorphic=no)`` etc...
+  :term:`Boolean attributes <boolean attribute>` are now specified using
+  key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`.
+  If the value is missing, the default is :n:`yes`.  The old syntax is still
+  supported, but produces the ``deprecated-attribute-syntax`` warning.
+
+  Deprecated attributes are :attr:`universes(monomorphic)`,
+  :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are
+  respectively replaced by :attr:`universes(polymorphic=no) <universes(polymorphic)>`,
+  :attr:`universes(template=no) <universes(template)>`
+  and :attr:`universes(cumulative=no) <universes(cumulative)>`.
   Attributes :attr:`program` and :attr:`canonical` are also affected,
-  with the syntax ``attr(false)`` being deprecated in favor of
-  ``attr=no``.
+  with the syntax :n:`@ident__attr(false)` being deprecated in favor of
+  :n:`@ident__attr=no`.
+
   (`#13312 <https://github.com/coq/coq/pull/13312>`_,
   by Emilio Jesus Gallego Arias).
-- 
cgit v1.2.3