Review commit: improving the doc of boolean attributes.

1 files changed, 13 insertions, 9 deletions

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).