Review commit: improving the doc of boolean attributes.

2 files changed, 35 insertions, 22 deletions

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 298ea4b4ab..104f84a253 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -99,15 +99,15 @@ coercions.
 
    Enables the program mode, in which 1) typechecking allows subset coercions and
    2) the elaboration of pattern matching of :cmd:`Fixpoint` and
-   :cmd:`Definition` act as if the :attr:`program` attribute had been
+   :cmd:`Definition` acts as if the :attr:`program` attribute has been
    used, generating obligations if there are unresolved holes after
    typechecking.
 
-.. attr:: program
+.. attr:: program{? = {| yes | no } }
    :name: program; Program
 
-   Allows using the Program mode on a specific
-   definition.  An alternative syntax is to use the legacy ``Program``
+   This :term:`boolean attribute` allows using or disabling the Program mode on a specific
+   definition.  An alternative and commonly used syntax is to use the legacy ``Program``
    prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter.
 
 .. _syntactic_control:
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index a2ed23335e..3790f36e5a 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -122,25 +122,32 @@ in a universe strictly higher than :g:`Set`.
 Polymorphic, Monomorphic
 -------------------------
 
-.. attr:: universes(polymorphic)
-   :name: universes(polymorphic); Polymorphic
+.. attr:: universes(polymorphic{? = {| yes | no } })
+   :name: universes(polymorphic); Polymorphic; Monomorphic
 
-   This boolean attribute can be used to control whether universe
+   This :term:`boolean attribute` can be used to control whether universe
    polymorphism is enabled in the definition of an inductive type.
    There is also a legacy syntax using the ``Polymorphic`` prefix (see
    :n:`@legacy_attr`) which, as shown in the examples, is more
    commonly used.
 
-   When ``polymorphic=no`` is set, global universe constraints
+   When ``universes(polymorphic=no)`` is used, global universe constraints
    are produced, even when the :flag:`Universe Polymorphism` flag is
    on. There is also a legacy syntax using the ``Monomorphic`` prefix
    (see :n:`@legacy_attr`).
 
+.. attr:: universes(monomorphic)
+
+   .. deprecated:: 8.13
+
+      Use :attr:`universes(polymorphic=no) <universes(polymorphic)>`
+      instead.
+
 .. flag:: Universe Polymorphism
 
    This flag is off by default.  When it is on, new declarations are
-   polymorphic unless the :attr:`universes(polymorphic)` attribute is
-   used to override the default.
+   polymorphic unless the :attr:`universes(polymorphic=no) <universes(polymorphic)>`
+   attribute is used to override the default.
 
 Many other commands can be used to declare universe polymorphic or
 monomorphic constants depending on whether the :flag:`Universe
@@ -168,18 +175,23 @@ attribute is used:
 Cumulative, NonCumulative
 -------------------------
 
-.. attr:: universes(cumulative)
-   :name: universes(cumulative); Cumulative
+.. attr:: universes(cumulative{? = {| yes | no } })
+   :name: universes(cumulative); Cumulative; NonCumulative
 
    Polymorphic inductive types, coinductive types, variants and
-   records can be declared cumulative using this attribute or the
-   legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as
+   records can be declared cumulative using this :term:`boolean attribute`
+   or the legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as
    shown in the examples, is more commonly used.
 
    This means that two instances of the same inductive type (family)
    are convertible based on the universe variances; they do not need
    to be equal.
 
+   When the attribtue is off, the inductive type is non-cumulative
+   even if the :flag:`Polymorphic Inductive Cumulativity` flag is on.
+   There is also a legacy syntax using the ``NonCumulative`` prefix
+   (see :n:`@legacy_attr`).
+
    This means that two instances of the same inductive type (family)
    are convertible only if all the universes are equal.
 
@@ -192,20 +204,21 @@ Cumulative, NonCumulative
 
    .. note::
 
-      ``#[ universes(polymorphic), universes(cumulative) ]`` can be
-      abbreviated into ``#[ universes(polymorphic, cumulative) ]``.
+      :n:`#[ universes(polymorphic{? = yes }), universes(cumulative{? = {| yes | no } }) ]` can be
+      abbreviated into :n:`#[ universes(polymorphic{? = yes }, cumulative{? = {| yes | no } }) ]`.
 
-   When the attribtue is off, the inductive type as non-cumulative
-   even if the :flag:`Polymorphic Inductive Cumulativity` flag is on.
-   There is also a legacy syntax using the ``NonCumulative`` prefix
-   (see :n:`@legacy_attr`).
+.. attr:: universes(noncumulative)
+
+   .. deprecated:: 8.13
+
+      Use :attr:`universes(cumulative=no) <universes(cumulative)>` instead.
 
 .. flag:: Polymorphic Inductive Cumulativity
 
    When this flag is on (it is off by default), it makes all
    subsequent *polymorphic* inductive definitions cumulative, unless
-   the :attr:`universes(cumulative)` attribute with setting ``off`` is
-   used.  It has no effect on *monomorphic* inductive definitions.
+   the :attr:`universes(cumulative=no) <universes(cumulative)>` attribute is
+   used to override the default.  It has no effect on *monomorphic* inductive definitions.
 
 Consider the examples below.