Review commit: improving the doc of boolean attributes.

3 files changed, 28 insertions, 20 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
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index ec3e3e8aa6..f7ce7f1c6c 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -87,7 +87,8 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
 
-.. attr:: canonical
+.. attr:: canonical{? = {| yes | no } }
+   :name: canonical
 
    This boolean attribute can decorate a :cmd:`Definition` or
    :cmd:`Let` command.  It is equivalent to having a :cmd:`Canonical
@@ -106,7 +107,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          #[canonical=no] Prf_equiv : equivalence Carrier Equal
 
-   See :ref:`canonicalstructures` for a more realistic example.
+   See :ref:`hierarchy_of_structures` for a more realistic example.
 
 .. cmd:: Print Canonical Projections {* @reference }
 
@@ -245,6 +246,8 @@ for each component of the pair. The declaration associates to the key ``*``
 relation ``pair_eq`` whenever the type constructor ``*`` is applied to two
 types being themselves in the ``EQ`` class.
 
+.. _hierarchy_of_structures:
+
 Hierarchy of structures
 ----------------------------