Fix doc for universes(foo) attributes

Fix #10570

2 files changed, 14 insertions, 12 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 54aeed428f..4beaff70f5 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1200,7 +1200,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 ``notemplate`` attribute.
+   This can be prevented using the ``universes(notemplate)``
+   attribute.
 
 .. warn:: Automatically declaring @ident as template polymorphic.
 
@@ -1208,9 +1209,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    implicitly declared template polymorphic by :flag:`Auto Template
    Polymorphism`.
 
-   An inductive type can be forced to be template polymorphic using the
-   ``template`` attribute: it should then fulfill the criterion to
-   be template polymorphic or an error is raised.
+   An inductive type can be forced to be template polymorphic using
+   the ``universes(template)`` attribute: it should then fulfill the
+   criterion to be template polymorphic or an error is raised.
 
 .. exn:: Inductive @ident cannot be made template polymorphic.
 
@@ -1221,7 +1222,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    Template polymorphism and universe polymorphism (see Chapter
    :ref:`polymorphicuniverses`) are incompatible, so if the later is
    enabled it will prevail over automatic template polymorphism and
-   cause an error when using the ``template`` attribute.
+   cause an error when using the ``universes(template)`` attribute.
 
 .. flag:: Template Check
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index f667dd94b0..94e9ccf0d4 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1503,19 +1503,20 @@ Each attribute has a name (an identifier) and may have a value.
 A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign),
 or a list of attributes, enclosed within brackets.
 
-Currently,
-the following attributes names are recognized:
+Some attributes are specific to a command, and so are described with
+that command. Currently, the following attributes are recognized by a
+variety of commands:
 
-``monomorphic``, ``polymorphic``
-    Take no value, analogous to the ``Monomorphic`` and ``Polymorphic`` flags
-    (see :ref:`polymorphicuniverses`).
+``universes(monomorphic)``, ``universes(polymorphic)``
+    Equivalent to the ``Monomorphic`` and
+    ``Polymorphic`` flags (see :ref:`polymorphicuniverses`).
 
 ``program``
-    Takes no value, analogous to the ``Program`` flag
+    Takes no value, equivalent to the ``Program`` flag
     (see :ref:`programs`).
 
 ``global``, ``local``
-    Take no value, analogous to the ``Global`` and ``Local`` flags
+    Take no value, equivalent to the ``Global`` and ``Local`` flags
     (see :ref:`controlling-locality-of-commands`).
 
 ``deprecated``