Review commit: improving the doc of boolean attributes.

2 files changed, 23 insertions, 18 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index ea29da6dd4..2b262b89c0 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -380,24 +380,22 @@ this attribute`.
 The order of top-level attributes doesn't affect their meaning.  ``#[foo,bar]``, ``#[bar,foo]``,
 ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent.
 
-Boolean attributes take the form ``attr={yes,no}``, when the key is
-omitted the default is assumed to be ``yes``.
+:gdef:`Boolean attributes <boolean attribute>` take the form :n:`@ident__attr{? = {| yes | no } }`.
+When the :n:`{| yes | no }` value is omitted, the default is :n:`yes`.
 
 The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax
 for certain attributes.  They are equivalent to new attributes as follows:
 
-================  ================================
-Legacy attribute  New attribute
-================  ================================
-`Local`           :attr:`local`
-`Global`          :attr:`global`
-`Polymorphic`     :attr:`universes(polymorphic)`
-`Monomorphic`     :attr:`universes(polymorphic)`
-`Cumulative`      :attr:`universes(cumulative)`
-`NonCumulative`   :attr:`universes(cumulative)`
-`Private`         :attr:`private(matching)`
-`Program`         :attr:`program`
-================  ================================
+=============================  ================================
+Legacy attribute               New attribute
+=============================  ================================
+`Local`                        :attr:`local`
+`Global`                       :attr:`global`
+`Polymorphic`, `Monomorphic`   :attr:`universes(polymorphic)`
+`Cumulative`, `NonCumulative`  :attr:`universes(cumulative)`
+`Private`                      :attr:`private(matching)`
+`Program`                      :attr:`program`
+=============================  ================================
 
 Attributes appear in the HTML documentation in blue or gray boxes
 after the label "Attribute".  In the pdf, they appear after the
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index b9453650eb..251b5e4955 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -1056,8 +1056,8 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    at level :math:`\Type` (without annotations or hiding it behind a
    definition) template polymorphic if possible.
 
-   This can be prevented using the :attr:`universes(template)`
-   attribute with the ``=no`` setting.
+   This can be prevented using the :attr:`universes(template=no) <universes(template)>`
+   attribute.
 
    Template polymorphism and full universe polymorphism (see Chapter
    :ref:`polymorphicuniverses`) are incompatible, so if the latter is
@@ -1075,9 +1075,10 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    the :attr:`universes(template)` attribute: in this case, the
    warning is not emitted.
 
-.. attr:: universes(template)
+.. attr:: universes(template{? = {| yes | no } })
+   :name: universes(template)
 
-   This boolean attribute can be used to explicitly declare an
+   This :term:`boolean attribute` can be used to explicitly declare an
    inductive type as template polymorphic, whether the :flag:`Auto
    Template Polymorphism` flag is on or off.
 
@@ -1096,6 +1097,12 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    inductive type to be template polymorphic, even if the :flag:`Auto
    Template Polymorphism` flag is on.
 
+.. attr:: universes(notemplate)
+
+   .. deprecated:: 8.13
+
+      Use :attr:`universes(template=no) <universes(template)>` instead.
+
 In practice, the rule **Ind-Family** is used by Coq only when all the
 inductive types of the inductive definition are declared with an arity
 whose sort is in the Type hierarchy. Then, the polymorphism is over