Merge PR #7301: [sphinx] Backport forgotten updates during the migration & other improvements

3 files changed, 173 insertions, 178 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 5a2aa0a1f8..f6bab02673 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -917,45 +917,33 @@ condition* for a constant :math:`X` in the following cases:
   satisfies the nested positivity condition for :math:`X`
 
 
-For instance, if one considers the type
-
 .. example::
-  .. coqtop:: all
+   For instance, if one considers the following variant of a tree type
+   branching over the natural numbers:
+
+  .. coqtop:: in
 
-     Module TreeExample.
-     Inductive tree (A:Type) : Type :=
-     | leaf : tree A
-     | node : A -> (nat -> tree A) -> tree A.
+     Inductive nattree (A:Type) : Type :=
+     | leaf : nattree A
+     | node : A -> (nat -> nattree A) -> nattree A.
      End TreeExample.
      
-::
+    Then every instantiated constructor of ``nattree A`` satisfies the nested positivity
+    condition for ``nattree``:
 
-    [TODO Note: This commentary does not seem to correspond to the
-     preceding example.  Instead it is referring to the first example
-     in Inductive Definitions section.  It seems we should either
-     delete the preceding example and refer the the example above of
-     type `list A`, or else we should rewrite the commentary below.]
-     
-    Then every instantiated constructor of list A satisfies the nested positivity
-    condition for list
-      │
-      ├─ concerning type list A of constructor nil:
-      │    Type list A of constructor nil satisfies the positivity condition for list
-      │    because list does not appear in any (real) arguments of the type of that
-      |    constructor (primarily because list does not have any (real)
-      |    arguments) ... (bullet 1)
-      │
-      ╰─ concerning type ∀ A → list A → list A of constructor cons:
-           Type ∀ A : Type, A → list A → list A of constructor cons
-           satisfies the positivity condition for list because:
-           │
-           ├─ list occurs only strictly positively in Type ... (bullet 3)
-           │
-           ├─ list occurs only strictly positively in A ... (bullet 3)
-           │
-           ├─ list occurs only strictly positively in list A ... (bullet 4)
-           │
-           ╰─ list satisfies the positivity condition for list A ... (bullet 1)
+    + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for
+      ``nattree`` because ``nattree`` does not appear in any (real) arguments of the
+      type of that constructor (primarily because ``nattree`` does not have any (real)
+      arguments) ... (bullet 1)
+
+    + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the
+      positivity condition for ``nattree`` because:
+
+      - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3)
+
+      - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2)
+
+      - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1)
 
 .. _Correctness-rules:
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index a93e9b156d..8746897e75 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -30,7 +30,7 @@ expressions. In this sense, the ``Record`` construction allows defining
 
 In the expression:
 
-.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } }.
+.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } }
 
 the first identifier `ident` is the name of the defined record and `sort` is its
 type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted,
@@ -70,7 +70,7 @@ depends on both ``top`` and ``bottom``.
 Let us now see the work done by the ``Record`` macro. First the macro
 generates a variant type definition with just one constructor:
 
-.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)}.
+.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)}
 
 To build an object of type `ident`, one should provide the constructor
 |ident_0| with the appropriate number of terms filling the fields of the record.
@@ -105,15 +105,15 @@ to be all present if the missing ones can be inferred or prompted for
 
 This syntax can be disabled globally for printing by
 
-.. cmd:: Unset Printing Records.
+.. cmd:: Unset Printing Records
 
 For a given type, one can override this using either
 
-.. cmd:: Add Printing Record @ident.
+.. cmd:: Add Printing Record @ident
 
 to get record syntax or
 
-.. cmd:: Add Printing Constructor @ident.
+.. cmd:: Add Printing Constructor @ident
 
 to get constructor syntax.
 
@@ -475,7 +475,7 @@ of :g:`match` expressions.
 Printing nested patterns
 +++++++++++++++++++++++++
 
-.. opt:: Printing Matching.
+.. opt:: Printing Matching
 
 The Calculus of Inductive Constructions knows pattern-matching only
 over simple patterns. It is however convenient to re-factorize nested
@@ -491,7 +491,7 @@ in the same way as the |Coq| kernel handles them.
 Factorization of clauses with same right-hand side
 ++++++++++++++++++++++++++++++++++++++++++++++++++
 
-.. opt:: Printing Factorizable Match Patterns.
+.. opt:: Printing Factorizable Match Patterns
 
 When several patterns share the same right-hand side, it is additionally
 possible to share the clauses using disjunctive patterns. Assuming that the
@@ -501,7 +501,7 @@ printer to try to do this kind of factorization.
 Use of a default clause
 +++++++++++++++++++++++
 
-.. opt:: Printing Allow Default Clause.
+.. opt:: Printing Allow Default Clause
 
 When several patterns share the same right-hand side which do not depend on the
 arguments of the patterns, yet an extra factorization is possible: the
@@ -512,7 +512,7 @@ default) tells |Coq|'s printer to use a default clause when relevant.
 Printing of wildcard patterns
 ++++++++++++++++++++++++++++++
 
-.. opt:: Printing Wildcard.
+.. opt:: Printing Wildcard
 
 Some variables in a pattern may not occur in the right-hand side of
 the pattern-matching clause. When this option is on (default), the
@@ -524,7 +524,7 @@ pattern-matching clause are just printed using the wildcard symbol
 Printing of the elimination predicate
 +++++++++++++++++++++++++++++++++++++
 
-.. opt:: Printing Synth.
+.. opt:: Printing Synth
 
 In most of the cases, the type of the result of a matched term is
 mechanically synthesizable. Especially, if the result type does not
@@ -539,23 +539,23 @@ Printing matching on irrefutable patterns
 If an inductive type has just one constructor, pattern-matching can be
 written using the first destructuring let syntax.
 
-.. cmd:: Add Printing Let @ident.
+.. cmd:: Add Printing Let @ident
 
    This adds `ident` to the list of inductive types for which pattern-matching
    is written using a let expression.
 
-.. cmd:: Remove Printing Let @ident.
+.. cmd:: Remove Printing Let @ident
 
    This removes ident from this list. Note that removing an inductive
    type from this list has an impact only for pattern-matching written
    using :g:`match`. Pattern-matching explicitly written using a destructuring
    :g:`let` are not impacted.
 
-.. cmd:: Test Printing Let for @ident.
+.. cmd:: Test Printing Let for @ident
 
    This tells if `ident` belongs to the list.
 
-.. cmd:: Print Table Printing Let.
+.. cmd:: Print Table Printing Let
 
    This prints the list of inductive types for which pattern-matching is
    written using a let expression.
@@ -571,20 +571,20 @@ Printing matching on booleans
 If an inductive type is isomorphic to the boolean type, pattern-matching
 can be written using ``if`` … ``then`` … ``else`` …:
 
-.. cmd:: Add Printing If @ident.
+.. cmd:: Add Printing If @ident
 
    This adds ident to the list of inductive types for which pattern-matching is
    written using an if expression.
 
-.. cmd:: Remove Printing If @ident.
+.. cmd:: Remove Printing If @ident
 
    This removes ident from this list.
 
-.. cmd:: Test Printing If for @ident.
+.. cmd:: Test Printing If for @ident
 
    This tells if ident belongs to the list.
 
-.. cmd:: Print Table Printing If.
+.. cmd:: Print Table Printing If
 
    This prints the list of inductive types for which pattern-matching is
    written using an if expression.
@@ -622,7 +622,7 @@ Advanced recursive functions
 
 The following experimental command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``:
 
-.. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term.
+.. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term
 
 This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper
 for several ways of defining a function *and other useful related
@@ -689,11 +689,11 @@ presence of partial application of `wrong` in the body of
 For now, dependent cases are not treated for non structurally
 terminating functions.
 
-.. exn:: The recursive argument must be specified
-.. exn:: No argument name @ident
-.. exn:: Cannot use mutual definition with well-founded recursion or measure
+.. exn:: The recursive argument must be specified.
+.. exn:: No argument name @ident.
+.. exn:: Cannot use mutual definition with well-founded recursion or measure.
 
-.. warn:: Cannot define graph for @ident
+.. warn:: Cannot define graph for @ident.
 
     The generation of the graph relation (`R_ident`) used to compute the induction scheme of ident
     raised a typing error. Only `ident` is defined; the induction scheme
@@ -703,12 +703,12 @@ terminating functions.
       which ``Function`` cannot deal with yet.
     - the definition is not a *pattern-matching tree* as explained above.
 
-.. warn:: Cannot define principle(s) for @ident
+.. warn:: Cannot define principle(s) for @ident.
 
      The generation of the graph relation (`R_ident`) succeeded but the induction principle
      could not be built. Only `ident` is defined. Please report.
 
-.. warn:: Cannot build functional inversion principle
+.. warn:: Cannot build functional inversion principle.
 
      `functional inversion` will not be available for the function.
 
@@ -782,12 +782,12 @@ structured sections. Then local declarations become available (see
 Section :ref:`gallina-definitions`).
 
 
-.. cmd:: Section @ident.
+.. cmd:: Section @ident
 
    This command is used to open a section named `ident`.
 
 
-.. cmd:: End @ident.
+.. cmd:: End @ident
 
     This command closes the section named `ident`. After closing of the
     section, the local declarations (variables and local definitions) get
@@ -820,7 +820,7 @@ Section :ref:`gallina-definitions`).
     Notice the difference between the value of `x’` and `x’’` inside section
     `s1` and outside.
 
-    .. exn:: This is not the last opened section
+    .. exn:: This is not the last opened section.
 
 **Remarks:**
 
@@ -852,25 +852,25 @@ In the syntax of module application, the ! prefix indicates that any
 (see the ``Module Type`` command below).
 
 
-.. cmd:: Module @ident.
+.. cmd:: Module @ident
 
    This command is used to start an interactive module named `ident`.
 
-.. cmdv:: Module @ident {* @module_binding}.
+.. cmdv:: Module @ident {* @module_binding}
 
    Starts an interactive functor with
    parameters given by module_bindings.
 
-.. cmdv:: Module @ident : @module_type.
+.. cmdv:: Module @ident : @module_type
 
    Starts an interactive module specifying its module type.
 
-.. cmdv:: Module @ident {* @module_binding} : @module_type.
+.. cmdv:: Module @ident {* @module_binding} : @module_type
 
    Starts an interactive functor with parameters given by the list of `module binding`, and output module
    type `module_type`.
 
-.. cmdv:: Module @ident <: {+<: @module_type }.
+.. cmdv:: Module @ident <: {+<: @module_type }
 
    Starts an interactive module satisfying each `module_type`.
 
@@ -879,14 +879,14 @@ In the syntax of module application, the ! prefix indicates that any
    Starts an interactive functor with parameters given by the list of `module_binding`. The output module type
    is verified against each `module_type`.
 
-.. cmdv:: Module [ Import | Export ].
+.. cmdv:: Module [ Import | Export ]
 
    Behaves like ``Module``, but automatically imports or exports the module.
 
 Reserved commands inside an interactive module
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Include @module.
+.. cmd:: Include @module
 
    Includes the content of module in the current
    interactive module. Here module can be a module expression or a module
@@ -894,11 +894,11 @@ Reserved commands inside an interactive module
    expression then the system tries to instantiate module by the current
    interactive module.
 
-.. cmd:: Include {+<+ @module}.
+.. cmd:: Include {+<+ @module}
 
    is a shortcut for the commands ``Include`` `module` for each `module`.
 
-.. cmd:: End @ident.
+.. cmd:: End @ident
 
    This command closes the interactive module `ident`. If the module type
    was given the content of the module is matched against it and an error
@@ -906,40 +906,40 @@ Reserved commands inside an interactive module
    functor) its components (constants, inductive types, submodules etc.)
    are now available through the dot notation.
 
-    .. exn:: No such label @ident
+    .. exn:: No such label @ident.
 
-    .. exn:: Signature components for label @ident do not match
+    .. exn:: Signature components for label @ident do not match.
 
-    .. exn:: This is not the last opened module
+    .. exn:: This is not the last opened module.
 
-.. cmd:: Module @ident := @module_expression.
+.. cmd:: Module @ident := @module_expression
 
     This command defines the module identifier `ident` to be equal
     to `module_expression`.
 
-    .. cmdv:: Module @ident {* @module_binding} := @module_expression.
+    .. cmdv:: Module @ident {* @module_binding} := @module_expression
 
        Defines a functor with parameters given by the list of `module_binding` and body `module_expression`.
 
-    .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression.
+    .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression
 
        Defines a functor with parameters given by the list of `module_binding` (possibly none), and output module type `module_type`,
        with body `module_expression`.
 
-    .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression.
+    .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression
 
        Defines a functor with parameters given by module_bindings (possibly none) with body `module_expression`.
        The body is checked against each |module_type_i|.
 
-    .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression}.
+    .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression}
 
        is equivalent to an interactive module where each `module_expression` is included.
 
-.. cmd:: Module Type @ident.
+.. cmd:: Module Type @ident
 
 This command is used to start an interactive module type `ident`.
 
-    .. cmdv:: Module Type @ident {* @module_binding}.
+    .. cmdv:: Module Type @ident {* @module_binding}
 
        Starts an interactive functor type with parameters given by `module_bindings`.
 
@@ -947,11 +947,11 @@ This command is used to start an interactive module type `ident`.
 Reserved commands inside an interactive module type:
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Include @module.
+.. cmd:: Include @module
 
    Same as ``Include`` inside a module.
 
-.. cmd:: Include {+<+ @module}.
+.. cmd:: Include {+<+ @module}
 
    is a shortcut for the command ``Include`` `module` for each `module`.
 
@@ -961,30 +961,30 @@ Reserved commands inside an interactive module type:
    The instance of this assumption will be automatically expanded at functor application, except when
    this functor application is prefixed by a ``!`` annotation.
 
-.. cmd:: End @ident.
+.. cmd:: End @ident
 
    This command closes the interactive module type `ident`.
 
-   .. exn:: This is not the last opened module type
+   .. exn:: This is not the last opened module type.
 
-.. cmd:: Module Type @ident := @module_type.
+.. cmd:: Module Type @ident := @module_type
 
    Defines a module type `ident` equal to `module_type`.
 
-    .. cmdv:: Module Type @ident {* @module_binding} := @module_type.
+    .. cmdv:: Module Type @ident {* @module_binding} := @module_type
 
        Defines a functor type `ident` specifying functors taking arguments `module_bindings` and
        returning `module_type`.
 
-    .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type }.
+    .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type }
 
        is equivalent to an interactive module type were each `module_type` is included.
 
-.. cmd:: Declare Module @ident : @module_type.
+.. cmd:: Declare Module @ident : @module_type
 
    Declares a module `ident` of type `module_type`.
 
-    .. cmdv:: Declare Module @ident {* @module_binding} : @module_type.
+    .. cmdv:: Declare Module @ident {* @module_binding} : @module_type
 
        Declares a functor with parameters given by the list of `module_binding` and output module type
        `module_type`.
@@ -1170,7 +1170,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
 
 .. _import_qualid:
 
-.. cmd:: Import @qualid.
+.. cmd:: Import @qualid
 
     If `qualid` denotes a valid basic module (i.e. its module type is a
     signature), makes its components available by their short names.
@@ -1225,15 +1225,15 @@ qualified name.
        When the module containing the command Export qualid
        is imported, qualid is imported as well.
 
-    .. exn:: @qualid is not a module
+    .. exn:: @qualid is not a module.
 
     .. warn:: Trying to mask the absolute name @qualid!
 
-.. cmd:: Print Module @ident.
+.. cmd:: Print Module @ident
 
     Prints the module type and (optionally) the body of the module `ident`.
 
-.. cmd:: Print Module Type @ident.
+.. cmd:: Print Module Type @ident
 
     Prints the module type corresponding to `ident`.
 
@@ -1525,6 +1525,7 @@ force the given argument to be guessed by replacing it by “_”. If
 possible, the correct argument will be automatically generated.
 
 .. exn:: Cannot infer a term for this placeholder.
+   :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments)
 
    |Coq| was not able to deduce an instantiation of a “_”.
 
@@ -1587,7 +1588,7 @@ Declaring Implicit Arguments
 
 To set implicit arguments *a posteriori*, one can use the command:
 
-.. cmd:: Arguments @qualid {* @possibly_bracketed_ident }.
+.. cmd:: Arguments @qualid {* @possibly_bracketed_ident }
    :name: Arguments (implicits)
 
 where the list of `possibly_bracketed_ident` is a prefix of the list of
@@ -1601,7 +1602,7 @@ of `qualid`.
 
 Implicit arguments can be cleared with the following syntax:
 
-.. cmd:: Arguments @qualid : clear implicits.
+.. cmd:: Arguments @qualid : clear implicits
 
 .. cmdv:: Global Arguments @qualid {* @possibly_bracketed_ident }
 
@@ -1610,13 +1611,13 @@ Implicit arguments can be cleared with the following syntax:
    implicit arguments known from inside the section to be the ones
    declared by the command.
 
-.. cmdv:: Local Arguments @qualid {* @possibly_bracketed_ident }.
+.. cmdv:: Local Arguments @qualid {* @possibly_bracketed_ident }
 
    When in a module, tell not to activate the
    implicit arguments ofqualid declared by this command to contexts that
    require the module.
 
-.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } }.
+.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } }
 
    For names of constants, inductive types,
    constructors, lemmas which can only be applied to a fixed number of
@@ -1668,7 +1669,7 @@ Automatic declaration of implicit arguments
 |Coq| can also automatically detect what are the implicit arguments of a
 defined object. The command is just
 
-.. cmd:: Arguments @qualid : default implicits.
+.. cmd:: Arguments @qualid : default implicits
 
 The auto-detection is governed by options telling if strict,
 contextual, or reversible-pattern implicit arguments must be
@@ -1742,7 +1743,7 @@ appear strictly in the body of the type, they are implicit.
 Mode for automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Implicit Arguments.
+.. opt:: Implicit Arguments
 
 This option (off by default) allows to systematically declare implicit
 the arguments detectable as such. Auto-detection of implicit arguments is
@@ -1754,7 +1755,7 @@ arguments have to be considered or not.
 Controlling strict implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Strict Implicit.
+.. opt:: Strict Implicit
 
 When the mode for automatic declaration of implicit arguments is on,
 the default is to automatically set implicit only the strict implicit
@@ -1763,7 +1764,7 @@ implicit arguments. To relax this constraint and to set
 implicit all non strict implicit arguments by default, you can turn this
 option off.
 
-.. opt:: Strongly Strict Implicit.
+.. opt:: Strongly Strict Implicit
 
 Use this option (off by default) to capture exactly the strict implicit
 arguments and no more than the strict implicit arguments.
@@ -1773,7 +1774,7 @@ arguments and no more than the strict implicit arguments.
 Controlling contextual implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Contextual Implicit.
+.. opt:: Contextual Implicit
 
 By default, |Coq| does not automatically set implicit the contextual
 implicit arguments. You can turn this option on to tell |Coq| to also
@@ -1784,7 +1785,7 @@ infer contextual implicit argument.
 Controlling reversible-pattern implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Reversible Pattern Implicit.
+.. opt:: Reversible Pattern Implicit
 
 By default, |Coq| does not automatically set implicit the reversible-pattern
 implicit arguments. You can turn this option on to tell |Coq| to also infer
@@ -1795,7 +1796,7 @@ reversible-pattern implicit argument.
 Controlling the insertion of implicit arguments not followed by explicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Maximal Implicit Insertion.
+.. opt:: Maximal Implicit Insertion
 
 Assuming the implicit argument mode is on, this option (off by default)
 declares implicit arguments to be automatically inserted when a
@@ -1841,7 +1842,7 @@ Renaming implicit arguments
 
 Implicit arguments names can be redefined using the following syntax:
 
-.. cmd:: Arguments @qualid {* @name} : @rename.
+.. cmd:: Arguments @qualid {* @name} : @rename
 
 With the assert flag, ``Arguments`` can be used to assert that a given
 object has the expected number of arguments and that these arguments
@@ -1867,18 +1868,18 @@ Displaying what the implicit arguments are
 To display the implicit arguments associated to an object, and to know
 if each of them is to be used maximally or not, use the command
 
-.. cmd:: Print Implicit @qualid.
+.. cmd:: Print Implicit @qualid
 
 Explicit displaying of implicit arguments for pretty-printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Printing Implicit.
+.. opt:: Printing Implicit
 
 By default, the basic pretty-printing rules hide the inferable implicit
 arguments of an application. Turn this option on to force printing all
 implicit arguments.
 
-.. opt:: Printing Implicit Defensive.
+.. opt:: Printing Implicit Defensive
 
 By default, the basic pretty-printing rules display the implicit
 arguments that are not detected as strict implicit arguments. This
@@ -1910,9 +1911,9 @@ but succeeds in
 Deactivation of implicit arguments for parsing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Parsing Explicit.
+.. opt:: Parsing Explicit
 
-Turning this option on, deactivates the use of implicit arguments.
+Turning this option on (it is off by default) deactivates the use of implicit arguments.
 
 In this case, all arguments of constants, inductive types,
 constructors, etc, including the arguments declared as implicit, have
@@ -1932,7 +1933,7 @@ Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in
 structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that
 `qualid` is declared as a canonical structure using the command
 
-.. cmd:: Canonical Structure @qualid.
+.. cmd:: Canonical Structure @qualid
 
 Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
 solved during the type-checking process, `qualid` is used as a solution.
@@ -1973,11 +1974,11 @@ and ``B`` can be synthesized in the next statement.
 Remark: If a same field occurs in several canonical structure, then
 only the structure declared first as canonical is considered.
 
-.. cmdv:: Canonical Structure @ident := @term : @type.
+.. cmdv:: Canonical Structure @ident := @term : @type
 
-.. cmdv:: Canonical Structure @ident := @term.
+.. cmdv:: Canonical Structure @ident := @term
 
-.. cmdv:: Canonical Structure @ident : @type := @term.
+.. cmdv:: Canonical Structure @ident : @type := @term
 
 These are equivalent to a regular definition of `ident` followed by the declaration
 ``Canonical Structure`` `ident`.
@@ -2005,7 +2006,7 @@ It is possible to bind variable names to a given type (e.g. in a
 development using arithmetic, it may be convenient to bind the names `n`
 or `m` to the type ``nat`` of natural numbers). The command for that is
 
-.. cmd:: Implicit Types {+ @ident } : @type.
+.. cmd:: Implicit Types {+ @ident } : @type
 
 The effect of the command is to automatically set the type of bound
 variables starting with `ident` (either `ident` itself or `ident` followed by
@@ -2027,7 +2028,7 @@ case, this latter type is considered).
 
        Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
 
-.. cmdv:: Implicit Type @ident : @type.
+.. cmdv:: Implicit Type @ident : @type
 
   This is useful for declaring the implicit type of a single variable.
 
@@ -2066,7 +2067,7 @@ the ``Generalizable`` vernacular command to avoid unexpected
 generalizations when mistyping identifiers. There are several commands
 that specify which variables should be generalizable.
 
-.. cmd:: Generalizable All Variables.
+.. cmd:: Generalizable All Variables
 
    All variables are candidate for
    generalization if they appear free in the context under a
@@ -2074,16 +2075,16 @@ that specify which variables should be generalizable.
    of typos. In such cases, the context will probably contain some
    unexpected generalized variable.
 
-.. cmd:: Generalizable No Variables.
+.. cmd:: Generalizable No Variables
 
    Disable implicit generalization  entirely. This is the default behavior.
 
-.. cmd:: Generalizable (Variable | Variables) {+ @ident }.
+.. cmd:: Generalizable (Variable | Variables) {+ @ident }
 
    Allow generalization of the given identifiers only. Calling this command multiple times
    adds to the allowed identifiers.
 
-.. cmd:: Global Generalizable.
+.. cmd:: Global Generalizable
 
    Allows exporting the choice of generalizable variables.
 
@@ -2128,7 +2129,7 @@ to coercions are provided in :ref:`implicitcoercions`.
 Printing constructions in full
 ------------------------------
 
-.. opt:: Printing All.
+.. opt:: Printing All
 
 Coercions, implicit arguments, the type of pattern-matching, but also
 notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some
@@ -2147,7 +2148,7 @@ the high-level printing features, use the command ``Unset Printing All``.
 Printing universes
 ------------------
 
-.. opt:: Printing Universes.
+.. opt:: Printing Universes
 
 Turn this option on to activate the display of the actual level of each
 occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in
@@ -2158,7 +2159,7 @@ Constructions.
 The constraints on the internal level of the occurrences of Type
 (see :ref:`Sorts`) can be printed using the command
 
-.. cmd:: Print {? Sorted} Universes.
+.. cmd:: Print {? Sorted} Universes
    :name: Print Universes
 
 If the optional ``Sorted`` option is given, each universe will be made
@@ -2167,7 +2168,7 @@ ordering) in the universe hierarchy.
 
 This command also accepts an optional output filename:
 
-.. cmdv:: Print {? Sorted} Universes @string.
+.. cmdv:: Print {? Sorted} Universes @string
 
 If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
 language, and can be processed by Graphviz tools. The format is
@@ -2237,7 +2238,7 @@ with a named-goal selector, see :ref:`goal-selectors`).
 Explicit displaying of existential instances for pretty-printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Printing Existential Instances.
+.. opt:: Printing Existential Instances
 
 This option (off by default) activates the full display of how the
 context of an existential variable is instantiated at each of the
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index a9c4dd7588..46e684b122 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -551,32 +551,33 @@ has type :token:`type`.
 
 .. _Axiom:
 
-.. cmd:: Axiom @ident : @term.
+.. cmd:: Axiom @ident : @term
 
    This command links *term* to the name *ident* as its specification in
    the global context. The fact asserted by *term* is thus assumed as a
    postulate.
 
-.. exn:: @ident already exists (Axiom)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Axiom)
 
-.. cmdv:: Parameter @ident : @term.
+.. cmdv:: Parameter @ident : @term
    :name: Parameter
 
    Is equivalent to ``Axiom`` :token:`ident` : :token:`term`
 
-.. cmdv:: Parameter {+ @ident } : @term.
+.. cmdv:: Parameter {+ @ident } : @term
 
    Adds parameters with specification :token:`term`
 
-.. cmdv:: Parameter {+ ( {+ @ident } : @term ) }.
+.. cmdv:: Parameter {+ ( {+ @ident } : @term ) }
 
    Adds blocks of parameters with different specifications.
 
-.. cmdv:: Parameters {+ ( {+ @ident } : @term ) }.
+.. cmdv:: Parameters {+ ( {+ @ident } : @term ) }
 
    Synonym of ``Parameter``.
 
-.. cmdv:: Local Axiom @ident : @term.
+.. cmdv:: Local Axiom @ident : @term
 
    Such axioms are never made accessible through their unqualified name by
    :cmd:`Import` and its variants. You have to explicitly give their fully
@@ -587,7 +588,7 @@ has type :token:`type`.
 
    Is equivalent to ``Axiom`` :token:`ident` : :token:`term`.
 
-.. cmd:: Variable @ident : @term.
+.. cmd:: Variable @ident : @term
 
 This command links :token:`term` to the name :token:`ident` in the context of
 the current section (see Section :ref:`section-mechanism` for a description of
@@ -596,22 +597,23 @@ will be unknown and every object using this variable will be explicitly
 parametrized (the variable is *discharged*). Using the ``Variable`` command out
 of any section is equivalent to using ``Local Parameter``.
 
-.. exn:: @ident already exists (Variable)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Variable)
 
-.. cmdv:: Variable {+ @ident } : @term.
+.. cmdv:: Variable {+ @ident } : @term
 
    Links :token:`term` to each :token:`ident`.
 
-.. cmdv:: Variable {+ ( {+ @ident } : @term) }.
+.. cmdv:: Variable {+ ( {+ @ident } : @term) }
 
    Adds blocks of variables with different specifications.
 
-.. cmdv:: Variables {+ ( {+ @ident } : @term) }.
+.. cmdv:: Variables {+ ( {+ @ident } : @term) }
 
-.. cmdv:: Hypothesis {+ ( {+ @ident } : @term) }.
+.. cmdv:: Hypothesis {+ ( {+ @ident } : @term) }
    :name: Hypothesis
 
-.. cmdv:: Hypotheses {+ ( {+ @ident } : @term) }.
+.. cmdv:: Hypotheses {+ ( {+ @ident } : @term) }
 
 Synonyms of ``Variable``.
 
@@ -641,46 +643,47 @@ type which is the type of its body.
 A formal presentation of constants and environments is given in
 Section :ref:`typing-rules`.
 
-.. cmd:: Definition @ident := @term.
+.. cmd:: Definition @ident := @term
 
    This command binds :token:`term` to the name :token:`ident` in the environment,
    provided that :token:`term` is well-typed.
 
-.. exn:: @ident already exists (Definition)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Definition)
 
-.. cmdv:: Definition @ident : @term := @term.
+.. cmdv:: Definition @ident : @term := @term
 
    It checks that the type of :token:`term`:math:`_2` is definitionally equal to
    :token:`term`:math:`_1`, and registers :token:`ident` as being of type
    :token:`term`:math:`_1`, and bound to value :token:`term`:math:`_2`.
 
 
-.. cmdv:: Definition @ident {* @binder } : @term := @term.
+.. cmdv:: Definition @ident {* @binder } : @term := @term
 
    This is equivalent to ``Definition`` :token:`ident` : :g:`forall`
    :token:`binder`:math:`_1` … :token:`binder`:math:`_n`, :token:`term`:math:`_1` := 
    fun :token:`binder`:math:`_1` …
    :token:`binder`:math:`_n` => :token:`term`:math:`_2`.
 
-.. cmdv:: Local Definition @ident := @term.
+.. cmdv:: Local Definition @ident := @term
 
    Such definitions are never made accessible through their
    unqualified name by :cmd:`Import` and its variants.
    You have to explicitly give their fully qualified name to refer to them.
 
-.. cmdv:: Example @ident := @term.
+.. cmdv:: Example @ident := @term
 
-.. cmdv:: Example @ident : @term := @term.
+.. cmdv:: Example @ident : @term := @term
 
-.. cmdv:: Example @ident {* @binder } : @term := @term.
+.. cmdv:: Example @ident {* @binder } : @term := @term
 
 These are synonyms of the Definition forms.
 
-.. exn:: The term @term has type @type while it is expected to have type @type
+.. exn:: The term @term has type @type while it is expected to have type @type.
 
-See also :cmd:`Opaque`, :cmd:`Transparent`, :tac:`unfold`.
+See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
-.. cmd:: Let @ident := @term.
+.. cmd:: Let @ident := @term
 
 This command binds the value :token:`term` to the name :token:`ident` in the
 environment of the current section. The name :token:`ident` disappears when the
@@ -690,13 +693,14 @@ prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term`
 ``in``. Using the ``Let`` command out of any section is equivalent to using
 ``Local Definition``.
 
-.. exn:: @ident already exists (Let)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Let)
 
-.. cmdv:: Let @ident : @term := @term.
+.. cmdv:: Let @ident : @term := @term
 
-.. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}.
+.. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}
 
-.. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}.
+.. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}
 
 See also Sections :ref:`section-mechanism`, commands :cmd:`Opaque`,
 :cmd:`Transparent`, and tactic :tacn:`unfold`.
@@ -803,9 +807,9 @@ and to prove that if any natural number :g:`n` satisfies :g:`P` its double
 successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the
 structural induction principle we got for :g:`nat`.
 
-.. exn:: Non strictly positive occurrence of @ident in @type
+.. exn:: Non strictly positive occurrence of @ident in @type.
 
-.. exn:: The conclusion of @type is not valid; it must be built from @ident
+.. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
 Parametrized inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -864,7 +868,7 @@ that it disallows recursive definition of types (in particular lists cannot
 be defined with the Variant keyword). No induction scheme is generated for
 this variant, unless :opt:`Nonrecursive Elimination Schemes` is set.
 
-.. exn:: The @num th argument of @ident must be @ident in @type
+.. exn:: The @num th argument of @ident must be @ident in @type.
 
 New from Coq V8.1
 +++++++++++++++++
@@ -912,7 +916,7 @@ Mutually defined inductive types
 
 The definition of a block of mutually inductive types has the form:
 
-.. cmdv:: Inductive @ident : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident : @term := {? | } @ident : @type {* | @ident : @type }}.
+.. cmdv:: Inductive @ident : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident : @term := {? | } @ident : @type {* | @ident : @type }}
 
 It has the same semantics as the above ``Inductive`` definition for each
 :token:`ident` All :token:`ident` are simultaneously added to the environment.
@@ -924,7 +928,7 @@ parameters correspond to a local context in which the whole set of
 inductive declarations is done. For this reason, the parameters must be
 strictly the same for each inductive types The extended syntax is:
 
-.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type }}.
+.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type }}
 
 The typical example of a mutual inductive data type is the one for trees and
 forests. We assume given two types :g:`A` and :g:`B` as variables. It can
@@ -1037,7 +1041,7 @@ constructions.
 
 .. _Fixpoint:
 
-.. cmd:: Fixpoint @ident @params {struct @ident} : @type := @term.
+.. cmd:: Fixpoint @ident @params {struct @ident} : @type := @term
 
 This command allows defining functions by pattern-matching over inductive objects
 using a fixed point construction. The meaning of this declaration is to
@@ -1151,7 +1155,7 @@ The ``Fixpoint`` construction enjoys also the with extension to define functions
 over mutually defined inductive types or more generally any mutually recursive
 definitions.
 
-.. cmdv:: Fixpoint @ident @params {struct @ident} : @type := @term {* with @ident {+ @params} : @type := @term}.
+.. cmdv:: Fixpoint @ident @params {struct @ident} : @type := @term {* with @ident {+ @params} : @type := @term}
 
 allows to define simultaneously fixpoints.
 
@@ -1178,7 +1182,7 @@ induction principles. It is described in Section
 Definitions of recursive objects in co-inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: CoFixpoint @ident : @type := @term.
+.. cmd:: CoFixpoint @ident : @type := @term
 
 introduces a method for constructing an infinite object of a coinductive
 type. For example, the stream containing all natural numbers can be
@@ -1239,38 +1243,39 @@ inhabitant of the type) is interactively built using tactics. The interactive
 proof mode is described in Chapter :ref:`proofhandling` and the tactics in
 Chapter :ref:`Tactics`. The basic assertion command is:
 
-.. cmd:: Theorem @ident : @type.
+.. cmd:: Theorem @ident : @type
 
 After the statement is asserted, Coq needs a proof. Once a proof of
 :token:`type` under the assumptions represented by :token:`binders` is given and
 validated, the proof is generalized into a proof of forall , :token:`type` and
 the theorem is bound to the name :token:`ident` in the environment.
 
-.. exn:: The term @term has type @type which should be Set, Prop or Type
+.. exn:: The term @term has type @type which should be Set, Prop or Type.
 
-.. exn:: @ident already exists (Theorem)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Theorem)
 
    The name you provided is already defined. You have then to choose
    another name.
 
-.. cmdv:: Lemma @ident : @type.
+.. cmdv:: Lemma @ident : @type
    :name: Lemma
 
-.. cmdv:: Remark @ident : @type.
+.. cmdv:: Remark @ident : @type
    :name: Remark
 
-.. cmdv:: Fact @ident : @type.
+.. cmdv:: Fact @ident : @type
    :name: Fact
 
-.. cmdv:: Corollary @ident : @type.
+.. cmdv:: Corollary @ident : @type
    :name: Corollary
 
-.. cmdv:: Proposition @ident : @type.
+.. cmdv:: Proposition @ident : @type
    :name: Proposition
 
    These commands are synonyms of ``Theorem`` :token:`ident` : :token:`type`.
 
-.. cmdv:: Theorem @ident : @type {* with @ident : @type}.
+.. cmdv:: Theorem @ident : @type {* with @ident : @type}
 
    This command is useful for theorems that are proved by simultaneous induction
    over a mutually inductive assumption, or that assert mutually dependent
@@ -1292,7 +1297,7 @@ the theorem is bound to the name :token:`ident` in the environment.
    The command can be used also with :cmd:`Lemma`, :cmd:`Remark`, etc. instead of
    :cmd:`Theorem`.
 
-.. cmdv:: Definition @ident : @type.
+.. cmdv:: Definition @ident : @type
 
    This allows defining a term of type :token:`type` using the proof editing
    mode. It behaves as Theorem but is intended to be used in conjunction with
@@ -1303,20 +1308,20 @@ the theorem is bound to the name :token:`ident` in the environment.
 
    See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
-.. cmdv:: Let @ident : @type.
+.. cmdv:: Let @ident : @type
 
    Like Definition :token:`ident` : :token:`type`. except that the definition is
    turned into a let-in definition generalized over the declarations depending
    on it after closing the current section.
 
-.. cmdv:: Fixpoint @ident @binders with .
+.. cmdv:: Fixpoint @ident @binders with
 
    This generalizes the syntax of Fixpoint so that one or more bodies
    can be defined interactively using the proof editing mode (when a
    body is omitted, its type is mandatory in the syntax). When the block
    of proofs is completed, it is intended to be ended by Defined.
 
-.. cmdv:: CoFixpoint @ident with.
+.. cmdv:: CoFixpoint @ident with
 
    This generalizes the syntax of CoFixpoint so that one or more bodies
    can be defined interactively using the proof editing mode.
@@ -1334,7 +1339,8 @@ the theorem is bound to the name :token:`ident` in the environment.
    When the proof is completed it should be validated and put in the environment
    using the keyword Qed.
 
-.. exn:: @ident already exists (Qed)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Qed)
 
 .. note::
 
@@ -1361,7 +1367,7 @@ the theorem is bound to the name :token:`ident` in the environment.
    unfolded in conversion tactics (see :ref:`performingcomputations`,
    :cmd:`Opaque`, :cmd:`Transparent`).
 
-.. cmdv:: Admitted.
+.. cmdv:: Admitted
    :name: Admitted
 
    Turns the current asserted statement into an axiom and exits the proof mode.