[attributes] [doc] Documentation review by Théo.

Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>

4 files changed, 22 insertions, 14 deletions

diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index 43bbc8b40d..e9737f8712 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -27,7 +27,8 @@ More information on co-inductive definitions can be found in
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`private(matching)`, and :attr:`using` attributes.
+   :attr:`private(matching)`, :attr:`typing(universes)`,
+   :attr:`typing(positive)`, and :attr:`using` attributes.
 
 .. example::
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 57771c9036..95bb1b0e0c 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -90,8 +90,9 @@ Section :ref:`typing-rules`.
    computation on :n:`@term`.
 
    These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`program` (see :ref:`program_definition`),
-   :attr:`canonical` and :attr:`using` attributes.
+   :attr:`program` (see :ref:`program_definition`), :attr:`canonical`,
+   :attr:`typing(universes)`, :attr:`typing(guarded)`, and
+   :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
@@ -162,7 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
-   This command accepts the :attr:`using` attribute.
+   This command accepts the :attr:`typing(universes)`,
+   :attr:`typing(guarded)`, and :attr:`using` attributes.
 
    .. exn:: The term @term has type @type which should be Set, Prop or Type.
       :undocumented:
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index f277997094..86de059f28 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -32,7 +32,8 @@ Inductive types
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`typing(positive)`, and :attr:`private(matching)` attributes.
+   :attr:`typing(positive)`, :attr:`typing(universes)`, and
+   :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
    The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
@@ -51,8 +52,8 @@ Inductive types
 
       The types of the constructors have to satisfy a *positivity
       condition* (see Section :ref:`positivity`). This condition
-      ensures the soundness of the inductive definition. The
-      positivity checking can be disabled using the :flag:`Positivity
+      ensures the soundness of the inductive definition.
+      Positivity checking can be disabled using the :flag:`Positivity
       Checking` flag or the :attr:`typing(positive)` attribute (see
       :ref:`controlling-typing-flags`).
 
@@ -392,7 +393,8 @@ constructions.
    consequently :n:`forall {* @binder }, @type` and its value is equivalent
    to :n:`fun {* @binder } => @term`.
 
-   This command accepts the :attr:`program` attribute.
+   This command accepts the :attr:`program`,
+   :attr:`typing(universes)`, and :attr:`typing(guarded)` attributes.
 
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
    constraints on a special argument called the decreasing argument. They
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index b8160b7966..08534c9e07 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1152,10 +1152,11 @@ Controlling Typing Flags
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
    printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(guarded)
+.. attr:: typing(guarded{? = {| yes | no } })
+   :name: typing(guarded)
 
    Similar to :flag:`Guard Checking`, but on a per-declaration
-   basis. Takes ``yes/no`` as parameters, i.e. ``typing(guarded=no)``.
+   basis. Disable guard checking locally with ``typing(guarded=no)``.
 
 .. flag:: Positivity Checking
 
@@ -1164,10 +1165,11 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(positive)
+.. attr:: typing(positive{? = {| yes | no } })
+   :name: typing(positive)
 
    Similar to :flag:`Positivity Checking`, but on a per-declaration basis.
-   Takes ``yes/no`` as parameters, i.e. ``typing(positive=no)``.
+   Disable positivity checking locally with ``typing(positive=no)``.
 
 .. flag:: Universe Checking
 
@@ -1177,10 +1179,11 @@ Controlling Typing Flags
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
    argument (see :ref:`command-line-options`).
 
-.. attr:: typing(universes)
+.. attr:: typing(universes{? = {| yes | no } })
+   :name: typing(universes)
 
    Similar to :flag:`Universe Checking`, but on a per-declaration basis.
-   Takes ``yes/no`` as parameters, i.e. ``typing(universes=no)``.
+   Disable universe checking locally with ``typing(universe=no)``.
 
 .. cmd:: Print Typing Flags