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

22 files changed, 1583 insertions, 1713 deletions

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 1d3b661732..c4f0147728 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -46,7 +46,7 @@ the expressiveness of the theory remains the same. Once the stage of
 parsing has finished only simple patterns remain. Re-nesting of
 pattern is performed at printing time. An easy way to see the result
 of the expansion is to toggle off the nesting performed at printing
-(use here :opt:`Set Printing Matching`), then by printing the term with :cmd:`Print`
+(use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print`
 if the term is a constant, or using the command :cmd:`Check`.
 
 The extended ``match`` still accepts an optional *elimination predicate*
@@ -75,7 +75,7 @@ by:
 Multiple patterns
 -----------------
 
-Using multiple patterns in the definition of max lets us write:
+Using multiple patterns in the definition of ``max`` lets us write:
 
 .. coqtop:: in undo
 
@@ -273,7 +273,7 @@ This option (off by default) removes parameters from constructors in patterns:
      match l with
      | nil => nil
      | cons _ l' => l'
-     end)
+     end).
    Unset Asymmetric Patterns.
 
 Implicit arguments in patterns
@@ -430,7 +430,7 @@ become impossible branches. In an impossible branch, you can answer
 anything but False_rect unit has the advantage to be subterm of
 anything.
 
-To be concrete: the tail function can be written:
+To be concrete: the ``tail`` function can be written:
 
 .. coqtop:: in
 
@@ -591,24 +591,24 @@ generated expression and the original.
 Here is a summary of the error messages corresponding to each
 situation:
 
-.. exn:: The constructor @ident expects @num arguments
+.. exn:: The constructor @ident expects @num arguments.
 
    The variable ident is bound several times in pattern termFound a constructor
    of inductive type term while a constructor of term is expectedPatterns are
    incorrect (because constructors are not applied to the correct number of the
    arguments, because they are not linear or they are wrongly typed).
 
-.. exn:: Non exhaustive pattern-matching
+.. exn:: Non exhaustive pattern-matching.
 
    The pattern matching is not exhaustive.
 
 .. exn:: The elimination predicate term should be of arity @num (for non \
-         dependent case) or @num (for dependent case)
+         dependent case) or @num (for dependent case).
 
    The elimination predicate provided to match has not the expected arity.
 
 .. exn:: Unable to infer a match predicate
-         Either there is a type incompatibility or the problem involves dependencies
+         Either there is a type incompatibility or the problem involves dependencies.
 
    There is a type mismatch between the different branches. The user should
    provide an elimination predicate.
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 38365e4035..cb93d48a41 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -37,11 +37,11 @@ Generating ML Code
 The next two commands are meant to be used for rapid preview of
 extraction. They both display extracted term(s) inside |Coq|.
 
-.. cmd:: Extraction @qualid.
+.. cmd:: Extraction @qualid
 
    Extraction of the mentioned object in the |Coq| toplevel.
 
-.. cmd:: Recursive Extraction @qualid ... @qualid.
+.. cmd:: Recursive Extraction {+ @qualid }
 
    Recursive extraction of all the mentioned objects and
    all their dependencies in the |Coq| toplevel.
@@ -49,7 +49,7 @@ extraction. They both display extracted term(s) inside |Coq|.
 All the following commands produce real ML files. User can choose to
 produce one monolithic file or one file per |Coq| library.
 
-.. cmd:: Extraction "@file" @qualid ... @qualid.
+.. cmd:: Extraction "@file" {+ @qualid }
 
    Recursive extraction of all the mentioned objects and all
    their dependencies in one monolithic `file`.
@@ -57,36 +57,36 @@ produce one monolithic file or one file per |Coq| library.
    language to fulfill its syntactic conventions, keeping original
    names as much as possible.
   
-.. cmd:: Extraction Library @ident.
+.. cmd:: Extraction Library @ident
 
    Extraction of the whole |Coq| library ``ident.v`` to an ML module
    ``ident.ml``. In case of name clash, identifiers are here renamed
    using prefixes ``coq_``  or ``Coq_`` to ensure a session-independent
    renaming.
 
-.. cmd:: Recursive Extraction Library @ident.
+.. cmd:: Recursive Extraction Library @ident
 
    Extraction of the |Coq| library ``ident.v`` and all other modules 
    ``ident.v`` depends on.
 
-.. cmd:: Separate Extraction @qualid ... @qualid.
+.. cmd:: Separate Extraction {+ @qualid }
 
    Recursive extraction of all the mentioned objects and all
    their dependencies, just as ``Extraction "file"``,
    but instead of producing one monolithic file, this command splits
    the produced code in separate ML files, one per corresponding Coq
    ``.v`` file. This command is hence quite similar to
-   ``Recursive Extraction Library``, except that only the needed
+   :cmd:`Recursive Extraction Library`, except that only the needed
    parts of Coq libraries are extracted instead of the whole.
    The naming convention in case of name clash is the same one as
-   ``Extraction Library``: identifiers are here renamed using prefixes
+   :cmd:`Extraction Library`: identifiers are here renamed using prefixes
    ``coq_``  or ``Coq_``.
 
 The following command is meant to help automatic testing of
 the extraction, see for instance the ``test-suite`` directory
 in the |Coq| sources.
 
-.. cmd:: Extraction TestCompile @qualid ... @qualid.
+.. cmd:: Extraction TestCompile {+ @qualid }
 
    All the mentioned objects and all their dependencies are extracted
    to a temporary |OCaml| file, just as in ``Extraction "file"``. Then
@@ -104,9 +104,9 @@ Setting the target language
 The ability to fix target language is the first and more important
 of the extraction options. Default is ``OCaml``.
 
-.. cmd:: Extraction Language OCaml.
-.. cmd:: Extraction Language Haskell.
-.. cmd:: Extraction Language Scheme.
+.. cmd:: Extraction Language OCaml
+.. cmd:: Extraction Language Haskell
+.. cmd:: Extraction Language Scheme
 
 Inlining and optimizations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -131,14 +131,14 @@ order to produce more readable code.
 
 The type-preserving optimizations are controlled by the following |Coq| options:
 
-.. opt:: Extraction Optimize.
+.. opt:: Extraction Optimize
 
    Default is on. This controls all type-preserving optimizations made on
    the ML terms (mostly reduction of dummy beta/iota redexes, but also
    simplifications on Cases, etc). Turn this option off if you want a
    ML term as close as possible to the Coq term.
 
-.. opt:: Extraction Conservative Types.
+.. opt:: Extraction Conservative Types
 
    Default is off. This controls the non type-preserving optimizations
    made on ML terms (which try to avoid function abstraction of dummy
@@ -146,7 +146,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted
    code of ``e`` and ``t`` respectively.
 
-.. opt:: Extraction KeepSingleton.
+.. opt:: Extraction KeepSingleton
 
    Default is off. Normally, when the extraction of an inductive type
    produces a singleton type (i.e. a type with only one constructor, and
@@ -155,7 +155,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    The typical example is ``sig``. This option allows disabling this
    optimization when one wishes to preserve the inductive structure of types.
 
-.. opt:: Extraction AutoInline.
+.. opt:: Extraction AutoInline
 
    Default is on. The extraction mechanism inlines the bodies of
    some defined constants, according to some heuristics
@@ -163,22 +163,22 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    Those heuristics are not always perfect; if you want to disable
    this feature, turn this option off.
 
-.. cmd:: Extraction Inline @qualid ... @qualid.
+.. cmd:: Extraction Inline {+ @qualid }
 
    In addition to the automatic inline feature, the constants
    mentionned by this command will always be inlined during extraction.
 
-.. cmd:: Extraction NoInline @qualid ... @qualid.
+.. cmd:: Extraction NoInline {+ @qualid }
 
    Conversely, the constants mentionned by this command will
    never be inlined during extraction.
 
-.. cmd:: Print Extraction Inline. 
+.. cmd:: Print Extraction Inline
 
    Prints the current state of the table recording the custom inlinings 
    declared by the two previous commands. 
 
-.. cmd:: Reset Extraction Inline.
+.. cmd:: Reset Extraction Inline
 
    Empties the table recording the custom inlinings (see the
    previous commands).
@@ -213,7 +213,7 @@ code elimination performed during extraction, in a way which
 is independent but complementary to the main elimination
 principles of extraction (logical parts and types).
 
-.. cmd:: Extraction Implicit @qualid [ @ident ... @ident ].
+.. cmd:: Extraction Implicit @qualid [ {+ @ident } ]
 
    This experimental command allows declaring some arguments of
    `qualid` as implicit, i.e. useless in extracted code and hence to
@@ -223,11 +223,11 @@ principles of extraction (logical parts and types).
    by a number indicating its position, starting from 1.
 
 When an actual extraction takes place, an error is normally raised if the
-``Extraction Implicit`` declarations cannot be honored, that is
+:cmd:`Extraction Implicit` declarations cannot be honored, that is
 if any of the implicited variables still occurs in the final code.
 This behavior can be relaxed via the following option:
 
-.. opt:: Extraction SafeImplicits.
+.. opt:: Extraction SafeImplicits
 
    Default is on. When this option is off, a warning is emitted
    instead of an error if some implicited variables still occur in the
@@ -253,19 +253,19 @@ a closed term, and of course the system cannot guess the program which
 realizes an axiom.  Therefore, it is possible to tell the system
 what ML term corresponds to a given axiom. 
 
-.. cmd:: Extract Constant @qualid => @string.
+.. cmd:: Extract Constant @qualid => @string
 
    Give an ML extraction for the given constant.
    The `string` may be an identifier or a quoted string.
 
-.. cmd:: Extract Inlined Constant @qualid => @string.
+.. cmd:: Extract Inlined Constant @qualid => @string
 
    Same as the previous one, except that the given ML terms will
    be inlined everywhere instead of being declared via a ``let``.
 
    .. note::
-      This command is sugar for an ``Extract Constant`` followed
-      by a ``Extraction Inline``. Hence a ``Reset Extraction Inline``
+      This command is sugar for an :cmd:`Extract Constant` followed
+      by a :cmd:`Extraction Inline`. Hence a :cmd:`Reset Extraction Inline`
       will have an effect on the realized and inlined axiom.
 
 .. caution:: It is the responsibility of the user to ensure that the ML
@@ -285,7 +285,7 @@ Notice that in the case of type scheme axiom (i.e. whose type is an
 arity, that is a sequence of product finished by a sort), then some type
 variables have to be given (as quoted strings). The syntax is then:
 
-.. cmdv:: Extract Constant @qualid @string ... @string => @string.
+.. cmdv:: Extract Constant @qualid @string ... @string => @string
 
 The number of type variables is checked by the system. For example:
 
@@ -294,7 +294,7 @@ The number of type variables is checked by the system. For example:
    Axiom Y : Set -> Set -> Set.
    Extract Constant Y "'a" "'b" => " 'a * 'b ".
 
-Realizing an axiom via ``Extract Constant`` is only useful in the
+Realizing an axiom via :cmd:`Extract Constant` is only useful in the
 case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom
 have no computational content and hence will not appears in extracted
 terms. But a warning is nonetheless issued if extraction encounters a
@@ -314,7 +314,7 @@ The system also provides a mechanism to specify ML terms for inductive
 types and constructors. For instance, the user may want to use the ML
 native boolean type instead of |Coq| one. The syntax is the following:
 
-.. cmd:: Extract Inductive @qualid => @string [ @string ... @string ].
+.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ]
 
    Give an ML extraction for the given inductive type. You must specify
    extractions for the type itself (first `string`) and all its
@@ -322,7 +322,7 @@ native boolean type instead of |Coq| one. The syntax is the following:
    the ML extraction must be an ML inductive datatype, and the native
    pattern-matching of the language will be used.
 
-.. cmdv:: Extract Inductive @qualid => @string [ @string ... @string ] @string.
+.. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string
 
    Same as before, with a final extra `string` that indicates how to
    perform pattern-matching over this inductive type. In this form,
@@ -338,7 +338,7 @@ native boolean type instead of |Coq| one. The syntax is the following:
    into |OCaml| ``int``, the code to provide has type:
    ``(unit->'a)->(int->'a)->int->'a``.
 
-.. caution:: As for ``Extract Constant``, this command should be used with care:
+.. caution:: As for :cmd:`Extract Constant`, this command should be used with care:
 
   * The ML code provided by the user is currently **not** checked at all by
     extraction, even for syntax errors.
@@ -356,7 +356,7 @@ native boolean type instead of |Coq| one. The syntax is the following:
     ML type is an efficient representation. For instance, when extracting
     ``nat`` to |OCaml| ``int``, the function ``Nat.mul`` stays quadratic.
     It might be interesting to associate this translation with
-    some specific ``Extract Constant`` when primitive counterparts exist.
+    some specific :cmd:`Extract Constant` when primitive counterparts exist.
 
 Typical examples are the following:
 
@@ -388,7 +388,7 @@ As an example of translation to a non-inductive datatype, let's turn
 Avoiding conflicts with existing filenames
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-When using ``Extraction Library``, the names of the extracted files
+When using :cmd:`Extraction Library`, the names of the extracted files
 directly depends from the names of the |Coq| files. It may happen that
 these filenames are in conflict with already existing files, 
 either in the standard library of the target language or in other
@@ -396,16 +396,16 @@ code that is meant to be linked with the extracted code.
 For instance the module ``List`` exists both in |Coq| and in |OCaml|.
 It is possible to instruct the extraction not to use particular filenames.
 
-.. cmd:: Extraction Blacklist @ident ... @ident.
+.. cmd:: Extraction Blacklist {+ @ident }
 
    Instruct the extraction to avoid using these names as filenames
    for extracted code.
 
-.. cmd:: Print Extraction Blacklist.
+.. cmd:: Print Extraction Blacklist
 
    Show the current list of filenames the extraction should avoid.
 
-.. cmd:: Reset Extraction Blacklist.
+.. cmd:: Reset Extraction Blacklist
 
    Allow the extraction to use any filename.
 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index e4dea34874..f5237e4fbf 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -179,7 +179,7 @@ A parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm )`,
 :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)` can be
 declared with the following command:
 
-.. cmd::  Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident.
+.. cmd::  Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident
 
 after having required the ``Setoid`` module with the ``Require Setoid``
 command.
@@ -218,15 +218,15 @@ For Leibniz equality, we may declare:
     [reflexivity proved by @refl_equal A]
   ...
 
-Some tactics (``reflexivity``, ``symmetry``, ``transitivity``) work only on
+Some tactics (:tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`transitivity`) work only on
 relations that respect the expected properties. The remaining tactics
-(``replace``, ``rewrite`` and derived tactics such as ``autorewrite``) do not
+(`replace`, :tacn:`rewrite` and derived tactics such as :tacn:`autorewrite`) do not
 require any properties over the relation. However, they are able to
 replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident.
+.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident
 
 The command declares ``f`` as a parametric morphism of signature ``sig``. The
 identifier ``id`` gives a unique name to the morphism and it is used as
@@ -317,7 +317,7 @@ instance mechanism. The behavior on section close is to generalize the
 instances by the variables of the section (and possibly hypotheses
 used in the proofs of instance declarations) but not to export them in
 the rest of the development for proof search. One can use the
-``Existing Instance`` command to do so outside the section, using the name of the
+cmd:`Existing Instance` command to do so outside the section, using the name of the
 declared morphism suffixed by ``_Morphism``, or use the ``Global`` modifier
 for the corresponding class instance declaration
 (see :ref:`First Class Setoids and Morphisms <first-class-setoids-and-morphisms>`) at
@@ -427,7 +427,7 @@ equality over ordered lists) ``set_eq ==> set_eq ==> set_eq``
 ``multiset_eq ==> multiset_eq ==> multiset_eq`` (``multiset_eq``
 being the equality over unordered lists).
 
-To declare multiple signatures for a morphism, repeat the ``Add Morphism``
+To declare multiple signatures for a morphism, repeat the :cmd:`Add Morphism`
 command.
 
 When morphisms have multiple signatures it can be the case that a
@@ -530,8 +530,8 @@ Tactics enabled on user provided relations
 
 The following tactics, all prefixed by ``setoid_``, deal with arbitrary
 registered relations and morphisms. Moreover, all the corresponding
-unprefixed tactics (i.e. ``reflexivity``, ``symmetry``, ``transitivity``,
-``replace``, ``rewrite``) have been extended to fall back to their prefixed
+unprefixed tactics (i.e. :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`transitivity`,
+:tacn:`replace`, :tacn:`rewrite`) have been extended to fall back to their prefixed
 counterparts when the relation involved is not Leibniz equality.
 Notice, however, that using the prefixed tactics it is possible to
 pass additional arguments such as ``using relation``.
@@ -564,21 +564,23 @@ on a given type.
 
 Every derived tactic that is based on the unprefixed forms of the
 tactics considered above will also work up to user defined relations.
-For instance, it is possible to register hints for ``autorewrite`` that
+For instance, it is possible to register hints for :tacn:`autorewrite` that
 are not proof of Leibniz equalities. In particular it is possible to
-exploit ``autorewrite`` to simulate normalization in a term rewriting
+exploit :tacn:`autorewrite` to simulate normalization in a term rewriting
 system up to user defined equalities.
 
 
 Printing relations and morphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The ``Print Instances`` command can be used to show the list of currently
+.. cmd:: Print Instances
+
+This command can be used to show the list of currently
 registered ``Reflexive`` (using ``Print Instances Reflexive``), ``Symmetric``
 or ``Transitive`` relations, Equivalences, PreOrders, PERs, and Morphisms
 (implemented as ``Proper`` instances). When the rewriting tactics refuse
 to replace a term in a context because the latter is not a composition
-of morphisms, the ``Print Instances`` commands can be useful to understand
+of morphisms, the :cmd:`Print Instances` command can be useful to understand
 what additional morphisms should be registered.
 
 
@@ -596,7 +598,7 @@ packing together the reflexivity, symmetry and transitivity lemmas).
 Notice that the syntax is not completely backward compatible since the
 identifier was not required.
 
-.. cmd:: Add Morphism f : @ident.
+.. cmd:: Add Morphism f : @ident
 
 The latter command also is restricted to the declaration of morphisms
 without parameters. It is not fully backward compatible since the
@@ -610,11 +612,11 @@ Notice that several limitations of the old implementation have been
 lifted. In particular, it is now possible to declare several relations
 with the same carrier and several signatures for the same morphism.
 Moreover, it is now also possible to declare several morphisms having
-the same signature. Finally, the replace and rewrite tactics can be
+the same signature. Finally, the :tacn:`replace` and :tacn:`rewrite` tactics can be
 used to replace terms in contexts that were refused by the old
 implementation. As discussed in the next section, the semantics of the
-new ``setoid_rewrite`` command differs slightly from the old one and
-``rewrite``.
+new :tacn:`setoid_rewrite` tactic differs slightly from the old one and
+tacn:`rewrite`.
 
 
 Extensions
@@ -624,8 +626,9 @@ Extensions
 Rewriting under binders
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-warning:: Due to compatibility issues, this feature is enabled only
-when calling the ``setoid_rewrite`` tactics directly and not ``rewrite``.
+.. warning::
+   Due to compatibility issues, this feature is enabled only
+   when calling the :tacn:`setoid_rewrite` tactic directly and not :tacn:`rewrite`.
 
 To be able to rewrite under binding constructs, one must declare
 morphisms with respect to pointwise (setoid) equivalence of functions.
@@ -672,12 +675,12 @@ where ``list_equiv`` implements an equivalence on lists parameterized by
 an equivalence on the elements.
 
 Note that when one does rewriting with a lemma under a binder using
-``setoid_rewrite``, the application of the lemma may capture the bound
+:tacn:`setoid_rewrite`, the application of the lemma may capture the bound
 variable, as the semantics are different from rewrite where the lemma
-is first matched on the whole term. With the new ``setoid_rewrite``,
+is first matched on the whole term. With the new :tacn:`setoid_rewrite`,
 matching is done on each subterm separately and in its local
 environment, and all matches are rewritten *simultaneously* by
-default. The semantics of the previous ``setoid_rewrite`` implementation
+default. The semantics of the previous :tacn:`setoid_rewrite` implementation
 can almost be recovered using the ``at 1`` modifier.
 
 
@@ -710,7 +713,7 @@ defined constants as transparent by default. This may slow down the
 resolution due to a lot of unifications (all the declared ``Proper``
 instances are tried at each node of the search tree). To speed it up,
 declare your constant as rigid for proof search using the command
-``Typeclasses Opaque`` (see :ref:`TypeclassesTransparent`).
+:cmd:`Typeclasses Opaque`.
 
 Strategies for rewriting
 ------------------------
@@ -809,8 +812,8 @@ strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many
 rewritings as possible, starting from the bottom or the top of the
 term.
 
-Hint databases created for ``autorewrite`` can also be used
-by ``rewrite_strat`` using the ``hints`` strategy that applies any of the
+Hint databases created for :tacn:`autorewrite` can also be used
+by :tacn:`rewrite_strat` using the ``hints`` strategy that applies any of the
 lemmas at the current subterm. The ``terms`` strategy takes the lemma
 names directly as arguments. The ``eval`` strategy expects a reduction
 expression (see :ref:`performingcomputations`) and succeeds
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c48c2d7ce1..5f8c064840 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -65,7 +65,7 @@ conditions holds:
 We then write :g:`f : C >-> D`. The restriction on the type
 of coercions is called *the uniform inheritance condition*.
 
-.. note:: The abstract classe ``Sortclass`` can be used as a source class, but
+.. note:: The abstract class ``Sortclass`` can be used as a source class, but
           the abstract class ``Funclass`` cannot.
 
 To coerce an object :g:`t:C t₁..tₙ` of ``C`` towards ``D``, we have to
@@ -124,42 +124,42 @@ term consists of the successive application of its coercions.
 Declaration of Coercions
 -------------------------
 
-.. cmd:: Coercion @qualid : @class >-> @class.
+.. cmd:: Coercion @qualid : @class >-> @class
 
   Declares the construction denoted by `qualid` as a coercion between
   the two given classes.
 
-  .. exn:: @qualid not declared
-  .. exn:: @qualid is already a coercion
-  .. exn:: Funclass cannot be a source class
-  .. exn:: @qualid is not a function
-  .. exn:: Cannot find the source class of @qualid
-  .. exn:: Cannot recognize @class as a source class of @qualid
-  .. exn:: @qualid does not respect the uniform inheritance condition
+  .. exn:: @qualid not declared.
+  .. exn:: @qualid is already a coercion.
+  .. exn:: Funclass cannot be a source class.
+  .. exn:: @qualid is not a function.
+  .. exn:: Cannot find the source class of @qualid.
+  .. exn:: Cannot recognize @class as a source class of @qualid.
+  .. exn:: @qualid does not respect the uniform inheritance condition.
   .. exn:: Found target class ... instead of ...
 
-  .. warn:: Ambiguous path
+  .. warn:: Ambiguous path.
 
     When the coercion `qualid` is added to the inheritance graph, non
     valid coercion paths are ignored; they are signaled by a warning
     displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
 
-  .. cmdv:: Local Coercion @qualid : @class >-> @class.
+  .. cmdv:: Local Coercion @qualid : @class >-> @class
 
     Declares the construction denoted by `qualid` as a coercion local to
     the current section.
 
-  .. cmdv:: Coercion @ident := @term.
+  .. cmdv:: Coercion @ident := @term
 
     This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
     and then declares `ident` as a coercion between it source and its target.
 
-  .. cmdv:: Coercion @ident := @term : @type.
+  .. cmdv:: Coercion @ident := @term : @type
 
     This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
     and then declares `ident` as a coercion between it source and its target.
 
-  .. cmdv:: Local Coercion @ident := @term.
+  .. cmdv:: Local Coercion @ident := @term
 
     This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
     and then declares `ident` as a coercion between it source and its target.
@@ -202,7 +202,7 @@ grammar of inductive types from Figure :ref:`vernacular` as follows:
 Especially, if the extra ``>`` is present in a constructor
 declaration, this constructor is declared as a coercion.
 
-.. cmd:: Identity Coercion @ident : @class >-> @class.
+.. cmd:: Identity Coercion @ident : @class >-> @class
 
   If ``C`` is the source `class` and ``D`` the destination, we check
   that ``C`` is a constant with a body of the form
@@ -211,13 +211,13 @@ declaration, this constructor is declared as a coercion.
   function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`,
   and we declare it as an identity coercion between ``C`` and ``D``.
 
-  .. exn:: @class must be a transparent constant
+  .. exn:: @class must be a transparent constant.
 
-  .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident.
+  .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident
 
     Idem but locally to the current section.
 
-  .. cmdv:: SubClass @ident := @type.
+  .. cmdv:: SubClass @ident := @type
      :name: SubClass
 
     If `type` is a class `ident'` applied to some arguments then
@@ -229,7 +229,7 @@ declaration, this constructor is declared as a coercion.
 
       ``Identity Coercion`` `Id_ident_ident'` : `ident` ``>->`` `ident'`.
 
-  .. cmdv:: Local SubClass @ident := @type.
+  .. cmdv:: Local SubClass @ident := @type
 
     Same as before but locally to the current section.
 
@@ -237,19 +237,19 @@ declaration, this constructor is declared as a coercion.
 Displaying Available Coercions
 -------------------------------
 
-.. cmd:: Print Classes.
+.. cmd:: Print Classes
 
   Print the list of declared classes in the current context.
 
-.. cmd:: Print Coercions.
+.. cmd:: Print Coercions
 
   Print the list of declared coercions in the current context.
 
-.. cmd:: Print Graph.
+.. cmd:: Print Graph
 
   Print the list of valid coercion paths in the current context.
 
-.. cmd:: Print Coercion Paths @class @class.
+.. cmd:: Print Coercion Paths @class @class
 
   Print the list of valid coercion paths between the two given classes.
 
@@ -275,7 +275,7 @@ Classes as Records
 We allow the definition of *Structures with Inheritance* (or classes as records)
 by extending the existing :cmd:`Record` macro. Its new syntax is:
 
-.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
+.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }
 
    The first identifier `ident` is the name of the defined record and
    `sort` is its type. The optional identifier after ``:=`` is the name
@@ -291,7 +291,7 @@ by extending the existing :cmd:`Record` macro. Its new syntax is:
    (this may fail if the uniform inheritance condition is not
    satisfied).
 
-.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
+.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }
    :name: Structure
 
    This is a synonym of :cmd:`Record`.
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 4f8cc34d4a..f887a5feea 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -113,7 +113,7 @@ tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`.
 .. tacn:: lia
    :name: lia
 
-This tactic offers an alternative to the :tacn:`omega` and :tac:`romega`
+This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega`
 tactics. Roughly speaking, the deductive power of lia is the combined deductive
 power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear
 goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 20e40c5507..009efd0d25 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -12,14 +12,14 @@ This tactic does not need any parameter:
 
 .. tacn:: omega
 
-``omega`` solves a goal in Presburger arithmetic, i.e. a universally
+:tacn:`omega` solves a goal in Presburger arithmetic, i.e. a universally
 quantified formula made of equations and inequations. Equations may
 be specified either on the type ``nat`` of natural numbers or on
 the type ``Z`` of binary-encoded integer numbers. Formulas on
 ``nat`` are automatically injected into ``Z``.  The procedure
 may use any hypothesis of the current proof session to solve the goal.
 
-Multiplication is handled by ``omega`` but only goals where at
+Multiplication is handled by :tacn:`omega` but only goals where at
 least one of the two multiplicands of products is a constant are
 solvable. This is the restriction meant by "Presburger arithmetic".
 
@@ -29,7 +29,7 @@ In any case, the computation eventually stops.
 Arithmetical goals recognized by ``omega``
 ------------------------------------------
 
-``omega`` applied only to quantifier-free formulas built from the
+:tacn:`omega` applied only to quantifier-free formulas built from the
 connectors::
 
    /\  \/  ~  ->
@@ -38,11 +38,11 @@ on atomic formulas. Atomic formulas are built from the predicates::
 
    =  <  <=  >  >=
 
-on ``nat`` or ``Z``. In expressions of type ``nat``, ``omega`` recognizes::
+on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes::
 
    +  -  *  S  O  pred
 
-and in expressions of type ``Z``, ``omega`` recognizes numeral constants and::
+and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and::
 
    +  -  *  Z.succ Z.pred
 
@@ -53,32 +53,32 @@ were arbitrary variables of type ``nat`` or ``Z``.
 Messages from ``omega``
 -----------------------
 
-When ``omega`` does not solve the goal, one of the following errors
+When :tacn:`omega` does not solve the goal, one of the following errors
 is generated:
 
-.. exn:: omega can't solve this system
+.. exn:: omega can't solve this system.
 
   This may happen if your goal is not quantifier-free (if it is
-  universally quantified, try ``intros`` first; if it contains
-  existentials quantifiers too, ``omega`` is not strong enough to solve your
+  universally quantified, try :tacn:`intros` first; if it contains
+  existentials quantifiers too, :tacn:`omega` is not strong enough to solve your
   goal). This may happen also if your goal contains arithmetical
-  operators unknown from ``omega``. Finally, your goal may be really
+  operators unknown from :tacn:`omega`. Finally, your goal may be really
   wrong!
 
-.. exn:: omega: Not a quantifier-free goal
+.. exn:: omega: Not a quantifier-free goal.
 
   If your goal is universally quantified, you should first apply
-  ``intro`` as many time as needed.
+  :tacn:`intro` as many times as needed.
 
-.. exn:: omega: Unrecognized predicate or connective: @ident
+.. exn:: omega: Unrecognized predicate or connective: @ident.
 
 .. exn:: omega: Unrecognized atomic proposition: ...
 
-.. exn:: omega: Can't solve a goal with proposition variables
+.. exn:: omega: Can't solve a goal with proposition variables.
 
-.. exn:: omega: Unrecognized proposition
+.. exn:: omega: Unrecognized proposition.
 
-.. exn:: omega: Can't solve a goal with non-linear products
+.. exn:: omega: Can't solve a goal with non-linear products.
 
 .. exn:: omega: Can't solve a goal with equality on type ...
 
@@ -115,21 +115,23 @@ Options
 
 .. opt:: Stable Omega
 
-This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
-resets internal name counters to make executions of ``omega`` independent.
+   .. deprecated:: 8.5
+
+   This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
+   resets internal name counters to make executions of :tacn:`omega` independent.
 
 .. opt:: Omega UseLocalDefs
 
-This option (on by default) allows ``omega`` to use the bodies of local
-variables.
+   This option (on by default) allows :tacn:`omega` to use the bodies of local
+   variables.
 
 .. opt:: Omega System
 
-This option (off by default) activate the printing of debug information
+   This option (off by default) activate the printing of debug information
 
 .. opt:: Omega Action
 
-This option (off by default) activate the printing of debug information
+   This option (off by default) activate the printing of debug information
 
 Technical data
 --------------
@@ -149,7 +151,7 @@ Overview of the tactic
 Overview of the OMEGA decision procedure
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The OMEGA decision procedure involved in the ``omega`` tactic uses
+The OMEGA decision procedure involved in the :tacn:`omega` tactic uses
 a small subset of the decision procedure presented in :cite:`TheOmegaPaper`
 Here is an overview, look at the original paper for more information.
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index be30d1bc4a..b685e68e43 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -145,13 +145,14 @@ prove some goals to construct the final definitions.
 Program Definition
 ~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Definition @ident := @term.
+.. cmd:: Program Definition @ident := @term
 
    This command types the value term in Russell and generates proof
    obligations. Once solved using the commands shown below, it binds the
    final |Coq| term to the name ``ident`` in the environment.
 
-   .. exn:: @ident already exists (Program Definition)
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Program Definition)
 
    .. cmdv:: Program Definition @ident : @type := @term
 
@@ -166,7 +167,7 @@ Program Definition
       .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ...
 
 
-   .. cmdv:: Program Definition @ident @binders : @type := @term.
+   .. cmdv:: Program Definition @ident @binders : @type := @term
 
       This is equivalent to:
 
@@ -181,7 +182,7 @@ See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`un
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term.
+.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term
 
 The optional order annotation follows the grammar:
 
@@ -254,7 +255,7 @@ using the syntax:
 Program Lemma
 ~~~~~~~~~~~~~
 
-.. cmd:: Program Lemma @ident : @type.
+.. cmd:: Program Lemma @ident : @type
 
    The Russell language can also be used to type statements of logical
    properties. It will generate obligations, try to solve them
@@ -349,7 +350,7 @@ Frequently Asked Questions
 ---------------------------
 
 
-.. exn:: Ill-formed recursive definition
+.. exn:: Ill-formed recursive definition.
 
   This error can happen when one tries to define a function by structural
   recursion on a subset object, which means the |Coq| function looks like:
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index ae666a0d45..47d3a7d7cd 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -171,21 +171,21 @@ performs the simplification in the hypothesis named :n:`@ident`.
 Error messages:
 
 
-.. exn:: not a valid ring equation
+.. exn:: Not a valid ring equation.
 
   The conclusion of the goal is not provable in the corresponding ring theory.
 
-.. exn:: arguments of ring_simplify do not have all the same type 
+.. exn:: Arguments of ring_simplify do not have all the same type.
   
   ``ring_simplify`` cannot simplify terms of several rings at the same
   time. Invoke the tactic once per ring structure.
 
-.. exn:: cannot find a declared ring structure over @term
+.. exn:: Cannot find a declared ring structure over @term.
 
   No ring has been declared for the type of the terms to be simplified.
   Use ``Add Ring`` first.
 
-.. exn:: cannot find a declared ring structure for equality @term 
+.. exn:: Cannot find a declared ring structure for equality @term.
 
   Same as above is the case of the ``ring`` tactic.
 
@@ -303,7 +303,7 @@ following property:
 
 The syntax for adding a new ring is 
 
-.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}.
+.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}
 
 The :n:`@ident` is not relevant. It is just used for error messages. The
 :n:`@term` is a proof that the ring signature satisfies the (semi-)ring
@@ -396,18 +396,18 @@ div :n:`@term`
 
 Error messages:
 
-.. exn:: bad ring structure
+.. exn:: Bad ring structure.
 
   The proof of the ring structure provided is not
   of the expected type.
 
-.. exn:: bad lemma for decidability of equality
+.. exn:: Bad lemma for decidability of equality.
 
   The equality function
   provided in the case of a computational ring has not the expected
   type.
 
-.. exn:: ring operation should be declared as a morphism
+.. exn:: Ring operation should be declared as a morphism.
 
   A setoid associated to the carrier of the ring structure has been found, 
   but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`.
@@ -656,7 +656,7 @@ zero for the correctness of the algorithm.
 
 The syntax for adding a new field is 
 
-.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}.
+.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}
 
 The :n:`@ident` is not relevant. It is just used for error
 messages. :n:`@term` is a proof that the field signature satisfies the
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 3e95bd8c45..6c7258f9c5 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -68,8 +68,8 @@ the remaining fields, e.g.:
    Defined.
 
 One has to take care that the transparency of every field is
-determined by the transparency of the ``Instance`` proof. One can use
-alternatively the ``Program Instance`` variant which has richer facilities
+determined by the transparency of the :cmd:`Instance` proof. One can use
+alternatively the :cmd:`Program Instance` variant which has richer facilities
 for dealing with obligations.
 
 
@@ -269,12 +269,9 @@ the Existing Instance command to achieve the same effect.
 Summary of the commands
 -----------------------
 
+.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }
 
-.. _Class:
-
-.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }.
-
-   The ``Class`` command is used to declare a type class with parameters
+   The :cmd:`Class` command is used to declare a type class with parameters
    ``binders`` and fields the declared record fields.
 
 Variants:
@@ -299,12 +296,10 @@ Variants:
    This variant declares a class a posteriori from a constant or
    inductive definition. No methods or instances are defined.
 
-.. _Instance:
-
 .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
 
-The ``Instance`` command is used to declare a type class instance named
-``ident`` of the class ``Class`` with parameters ``t1`` to ``tn`` and
+The :cmd:`Instance` command is used to declare a type class instance named
+``ident`` of the class :cmd:`Class` with parameters ``t1`` to ``tn`` and
 fields ``b1`` to ``bi``, where each field must be a declared field of
 the class.  Missing fields must be filled in interactive proof mode.
 
@@ -314,112 +309,106 @@ optional priority can be declared, 0 being the highest priority as for
 auto hints. If the priority is not specified, it defaults to the number
 of non-dependent binders of the instance.
 
-..cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term
+.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term
 
    This syntax is used for declaration of singleton class instances or
    for directly giving an explicit term of type ``forall binders, Class
    t1 … tn``.  One need not even mention the unique field name for
    singleton classes.
 
-..cmdv:: Global Instance
+.. cmdv:: Global Instance
 
    One can use the ``Global`` modifier on instances declared in a
    section so that their generalization is automatically redeclared
    after the section is closed.
 
-..cmdv:: Program Instance
+.. cmdv:: Program Instance
+   :name: Program Instance
 
    Switches the type-checking to Program (chapter :ref:`programs`) and
    uses the obligation mechanism to manage missing fields.
 
-..cmdv:: Declare Instance
+.. cmdv:: Declare Instance
+   :name: Declare Instance
 
    In a Module Type, this command states that a corresponding concrete
-   instance should exist in any implementation of thisModule Type. This
-   is similar to the distinction betweenParameter vs. Definition, or
-   between Declare Module and Module.
+   instance should exist in any implementation of this Module Type. This
+   is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or
+   between :cmd:`Declare Module` and :cmd:`Module`.
 
 
-Besides the ``Class`` and ``Instance`` vernacular commands, there are a
+Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
 few other commands related to type classes.
 
-.. _ExistingInstance:
-
-Existing Instance
-~~~~~~~~~~~~~~~~~
-
 .. cmd:: Existing Instance {+ @ident} [| priority]
 
-This commands adds an arbitrary list of constants whose type ends with
-an applied type class to the instance database with an optional
-priority.  It can be used for redeclaring instances at the end of
-sections, or declaring structure projections as instances. This is
-equivalent to ``Hint Resolve ident : typeclass_instances``, except it
-registers instances for ``Print Instances``.
-
-.. _Context:
-
-Context
-~~~~~~~
+   This commands adds an arbitrary list of constants whose type ends with
+   an applied type class to the instance database with an optional
+   priority.  It can be used for redeclaring instances at the end of
+   sections, or declaring structure projections as instances. This is
+   equivalent to ``Hint Resolve ident : typeclass_instances``, except it
+   registers instances for :cmd:`Print Instances`.
 
 .. cmd:: Context @binders
 
-Declares variables according to the given binding context, which might
-use :ref:`implicit-generalization`.
+   Declares variables according to the given binding context, which might
+   use :ref:`implicit-generalization`.
 
 .. tacn:: typeclasses eauto
-
-This tactic uses a different resolution engine than :tacn:`eauto` and
-:tacn:`auto`. The main differences are the following:
-
-+ Contrary to ``eauto`` and ``auto``, the resolution is done entirely in
-  the new proof engine (as of Coq v8.6), meaning that backtracking is
-  available among dependent subgoals, and shelving goals is supported.
-  typeclasses eauto is a multi-goal tactic. It analyses the dependencies
-  between subgoals to avoid backtracking on subgoals that are entirely
-  independent.
-
-+ When called with no arguments, typeclasses eauto uses
-  thetypeclass_instances database by default (instead of core).
-  Dependent subgoals are automatically shelved, and shelved goals can
-  remain after resolution ends (following the behavior ofCoq 8.5).
-  *Note: * As of Coq 8.6, all:once (typeclasses eauto) faithfully
-  mimicks what happens during typeclass resolution when it is called
-  during refinement/type-inference, except that *only* declared class
-  subgoals are considered at the start of resolution during type
-  inference, while “all” can select non-class subgoals as well. It might
-  move to ``all:typeclasses eauto`` in future versions when the
-  refinement engine will be able to backtrack.
-
-+ When called with specific databases (e.g. with), typeclasses eauto
-  allows shelved goals to remain at any point during search and treat
-  typeclasses goals like any other.
-
-+ The transparency information of databases is used consistently for
-  all hints declared in them. It is always used when calling the
-  unifier. When considering the local hypotheses, we use the transparent
-  state of the first hint database given. Using an empty database
-  (created with Create HintDb for example) with unfoldable variables and
-  constants as the first argument of typeclasses eauto hence makes
-  resolution with the local hypotheses use full conversion during
-  unification.
-
-
-Variants:
-
-#. ``typeclasses eauto [num]``
-
-   *Warning:* The semantics for the limit num
-   is different than for auto. By default, if no limit is given the
-   search is unbounded. Contrary to auto, introduction steps (intro) are
-   counted, which might result in larger limits being necessary when
-   searching with typeclasses eauto than auto.
-
-#. ``typeclasses eauto with {+ @ident}``
-
-   This variant runs resolution with the given hint databases. It treats
-   typeclass subgoals the same as other subgoals (no shelving of
-   non-typeclass goals in particular).
+   :name: typeclasses eauto
+
+   This tactic uses a different resolution engine than :tacn:`eauto` and
+   :tacn:`auto`. The main differences are the following:
+
+   + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in
+     the new proof engine (as of Coq 8.6), meaning that backtracking is
+     available among dependent subgoals, and shelving goals is supported.
+     typeclasses eauto is a multi-goal tactic. It analyses the dependencies
+     between subgoals to avoid backtracking on subgoals that are entirely
+     independent.
+
+   + When called with no arguments, typeclasses eauto uses
+     the ``typeclass_instances`` database by default (instead of core).
+     Dependent subgoals are automatically shelved, and shelved goals can
+     remain after resolution ends (following the behavior of Coq 8.5).
+
+     .. note::
+        As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully
+        mimicks what happens during typeclass resolution when it is called
+        during refinement/type-inference, except that *only* declared class
+        subgoals are considered at the start of resolution during type
+        inference, while ``all`` can select non-class subgoals as well. It might
+        move to ``all:typeclasses eauto`` in future versions when the
+        refinement engine will be able to backtrack.
+
+   + When called with specific databases (e.g. with), typeclasses eauto
+     allows shelved goals to remain at any point during search and treat
+     typeclasses goals like any other.
+
+   + The transparency information of databases is used consistently for
+     all hints declared in them. It is always used when calling the
+     unifier. When considering the local hypotheses, we use the transparent
+     state of the first hint database given. Using an empty database
+     (created with :cmd:`Create HintDb` for example) with unfoldable variables and
+     constants as the first argument of typeclasses eauto hence makes
+     resolution with the local hypotheses use full conversion during
+     unification.
+
+
+   .. cmdv:: typeclasses eauto @num
+
+      .. warning::
+         The semantics for the limit :n:`@num`
+         is different than for auto. By default, if no limit is given the
+         search is unbounded. Contrary to auto, introduction steps (intro) are
+         counted, which might result in larger limits being necessary when
+         searching with typeclasses eauto than auto.
+
+   .. cmdv:: typeclasses eauto with {+ @ident}
+
+      This variant runs resolution with the given hint databases. It treats
+      typeclass subgoals the same as other subgoals (no shelving of
+      non-typeclass goals in particular).
 
 .. tacn:: autoapply @term with @ident
    :name: autoapply
@@ -441,34 +430,36 @@ Typeclasses Transparent, Typclasses Opaque
    This command defines makes the identifiers transparent during type class
    resolution.
 
-   .. cmdv:: Typeclasses Opaque {+ @ident}
-      :name: Typeclasses Opaque
+.. cmd:: Typeclasses Opaque {+ @ident}
+
+   Make the identifiers opaque for typeclass search. It is useful when some
+   constants prevent some unifications and make resolution fail. It is also
+   useful to declare constants which should never be unfolded during
+   proof-search, like fixpoints or anything which does not look like an
+   abbreviation. This can additionally speed up proof search as the typeclass
+   map can be indexed by such rigid constants (see
+   :ref:`thehintsdatabasesforautoandeauto`).
 
-      Make the identifiers opaque for typeclass search. It is useful when some
-      constants prevent some unifications and make resolution fail. It is also
-      useful to declare constants which should never be unfolded during
-      proof-search, like fixpoints or anything which does not look like an
-      abbreviation. This can additionally speed up proof search as the typeclass
-      map can be indexed by such rigid constants (see
-      :ref:`thehintsdatabasesforautoandeauto`).
+By default, all constants and local variables are considered transparent. One
+should take care not to make opaque any constant that is used to abbreviate a
+type, like:
 
-   By default, all constants and local variables are considered transparent. One
-   should take care not to make opaque any constant that is used to abbreviate a
-   type, like:
+::
 
-   ::
+   relation A := A -> A -> Prop.
 
-      relation A := A -> A -> Prop.
+This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
 
-   This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
 
+Options
+~~~~~~~
 
 .. opt:: Typeclasses Dependency Order
 
    This option (on by default since 8.6) respects the dependency order
    between subgoals, meaning that subgoals which are depended on by other
    subgoals come first, while the non-dependent subgoals were put before
-   the dependent ones previously (Coq v8.5 and below). This can result in
+   the dependent ones previously (Coq 8.5 and below). This can result in
    quite different performance behaviors of proof search.
 
 
@@ -530,6 +521,23 @@ Typeclasses Transparent, Typclasses Opaque
    solution to the typeclass goal of this class is found, we never
    backtrack on it, assuming that it is canonical.
 
+.. opt:: Typeclasses Debug {? Verbosity @num}
+
+   These options allow to see the resolution steps of typeclasses that are
+   performed during search. The ``Debug`` option is synonymous to ``Debug
+   Verbosity 1``, and ``Debug Verbosity 2`` provides more information
+   (tried tactics, shelving of goals, etc…).
+
+.. opt:: Refine Instance Mode
+
+   This option allows to switch the behavior of instance declarations made through
+   the Instance command.
+
+   + When it is on (the default), instances that have unsolved holes in
+     their proof-term silently open the proof mode with the remaining
+     obligations to prove.
+
+   + When it is off, they fail with an error instead.
 
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -546,26 +554,3 @@ Typeclasses eauto `:=`
      default) or breadth-first search.
 
    + ``depth`` This sets the depth limit of the search.
-
-
-Set Typeclasses Debug
-~~~~~~~~~~~~~~~~~~~~~
-
-.. opt:: Typeclasses Debug {? Verbosity @num}
-
-These options allow to see the resolution steps of typeclasses that are
-performed during search. The ``Debug`` option is synonymous to ``Debug
-Verbosity 1``, and ``Debug Verbosity 2`` provides more information
-(tried tactics, shelving of goals, etc…).
-
-
-.. opt:: Refine Instance Mode
-
-This options allows to switch the behavior of instance declarations made through
-the Instance command.
-
-+ When it is on (the default), instances that have unsolved holes in
-  their proof-term silently open the proof mode with the remaining
-  obligations to prove.
-
-+ When it is off, they fail with an error instead.
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index c791fc906b..e80cfb6bb5 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -79,7 +79,7 @@ levels.
 
 When printing :g:`pidentity`, we can see the universes it binds in
 the annotation :g:`@{Top.2}`. Additionally, when
-:g:`Set Printing Universes` is on we print the "universe context" of
+:opt:`Printing Universes` is on we print the "universe context" of
 :g:`pidentity` consisting of the bound universes and the
 constraints they must verify (for :g:`pidentity` there are no constraints).
 
@@ -169,7 +169,7 @@ declared cumulative using the :g:`Cumulative` prefix.
 
    Declares the inductive as cumulative
 
-Alternatively, there is an option :g:`Set Polymorphic Inductive
+Alternatively, there is an option :opt:`Polymorphic Inductive
 Cumulativity` which when set, makes all subsequent *polymorphic*
 inductive definitions cumulative.  When set, inductive types and the
 like can be enforced to be non-cumulative using the :g:`NonCumulative`
@@ -229,7 +229,7 @@ Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
 error is issued whenever the user uses the :g:`Cumulative` or
 :g:`NonCumulative` prefix in a monomorphic context.
-Notice that this is not the case for the option :g:`Set Polymorphic Inductive Cumulativity`.
+Notice that this is not the case for the option :opt:`Polymorphic Inductive Cumulativity`.
 That is, this option, when set, makes all subsequent *polymorphic*
 inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used)
 but has no effect on *monomorphic* inductive declarations.
@@ -367,7 +367,7 @@ Explicit Universes
 The syntax has been extended to allow users to explicitly bind names
 to universes and explicitly instantiate polymorphic definitions.
 
-.. cmd:: Universe @ident.
+.. cmd:: Universe @ident
 
    In the monorphic case, this command declares a new global universe
    named :g:`ident`, which can be referred to using its qualified name
@@ -378,7 +378,7 @@ to universes and explicitly instantiate polymorphic definitions.
    declarations in the same section.
 
 
-.. cmd:: Constraint @ident @ord @ident.
+.. cmd:: Constraint @ident @ord @ident
 
    This command declares a new constraint between named universes. The
    order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint
@@ -438,7 +438,7 @@ underscore or by omitting the annotation to a polymorphic definition.
 
 .. opt:: Strict Universe Declaration.
 
-   The command ``Unset Strict Universe Declaration`` allows one to freely use
+   Turning this option off allows one to freely use
    identifiers for universes without declaring them first, with the
    semantics that the first use declares it. In this mode, the universe
    names are not associated with the definition or proof once it has been
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 2963306075..136f9088b1 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -3,9 +3,6 @@
 .. include:: preamble.rst
 .. include:: replaces.rst
 
-Introduction
-===========================================
-
 .. include:: introduction.rst
 .. include:: credits.rst
 
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.
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 93dcfca4bf..83dddab4f5 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -171,7 +171,7 @@ and ``coqtop``, unless stated otherwise:
   Coq's auto-generated name scheme with names of the form *ident0*, *ident1*,
   etc. The command ``Set Mangle Names`` turns the behavior on in a document,
   and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature
-  s intended to be used as a linter for developments that want to be robust to
+  is intended to be used as a linter for developments that want to be robust to
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
 :-compat *version*: Attempt to maintain some backward-compatibility
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 59867988a4..59a88771a0 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -137,7 +137,7 @@ Here we describe only few of them.
    (e.g. wrappers)
 :COQ_SRC_SUBDIRS:
    can be extended by including other paths in which ``*.cm*`` files
-   are searched. For example ``COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq``
+   are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq``
    lets you build a plugin containing OCaml code that depends on the
    OCaml code of ``Unicoq``.
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 7ab11889f5..c5ee724caf 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -245,9 +245,10 @@ focused goals with:
    :name: ... : ... (goal selector)
 
    We can also use selectors as a tactical, which allows to use them nested
-   in a tactic expression, by using the keyword ``only``:
+   in a tactic expression, by using the keyword :tacn:`only`:
 
    .. tacv:: only selector : expr
+      :name: only ... : ...
 
       When selecting several goals, the tactic expr is applied globally to all
       selected goals.
@@ -268,6 +269,7 @@ focused goals with:
       for ``n-n`` when specifying multiple ranges.
 
    .. tacv:: all: @expr
+      :name: all: ...
 
       In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only
       be used at the toplevel of a tactic expression.
@@ -279,6 +281,7 @@ focused goals with:
       used at the toplevel of a tactic expression.
 
    .. tacv:: par: @expr
+      :name: par: ...
 
       In this variant, :n:`@expr` is applied to all focused goals in parallel.
       The number of workers can be controlled via the command line option
@@ -288,8 +291,8 @@ focused goals with:
       nothing (i.e. it cannot make some progress). ``par:`` can only be used at
       the toplevel of a tactic expression.
 
-   .. exn:: No such goal
-      :name: No such goal (goal selector)
+   .. exn:: No such goal.
+      :name: No such goal. (Goal selector)
 
    .. TODO change error message index entry
 
@@ -348,7 +351,7 @@ We can check if a tactic made progress with:
    to one of the focused subgoal produced subgoals equal to the initial
    goals (up to syntactical equality), then an error of level 0 is raised.
 
-   .. exn:: Failed to progress
+   .. exn:: Failed to progress.
 
 Backtracking branching
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -389,7 +392,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics:
    :n:`first [:@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first
    :n:`v__i` to have *at least* one success.
 
-   .. exn:: Error message: No applicable tactic
+   .. exn:: No applicable tactic.
 
    .. tacv:: first @expr
 
@@ -478,7 +481,7 @@ one* success:
       whether a second success exists, and may run further effects
       immediately.
 
-   .. exn:: This tactic has more than one success
+   .. exn:: This tactic has more than one success.
 
 Checking the failure
 ~~~~~~~~~~~~~~~~~~~~
@@ -516,7 +519,7 @@ among a panel of tactics:
    each goal independently, if it doesn’t solve the goal then it tries to
    apply :n:`v__2` and so on. It fails if there is no solving tactic.
 
-   .. exn:: Cannot solve the goal
+   .. exn:: Cannot solve the goal.
 
    .. tacv:: solve @expr
 
@@ -547,7 +550,7 @@ Failing
    :tacn:`fail` tactic will, however, succeed if all the goals have already been
    solved.
 
-   .. tacv:: fail @natural
+   .. tacv:: fail @num
 
       The number is the failure level. If no level is specified, it defaults to 0.
       The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
@@ -555,14 +558,14 @@ Failing
       (backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`,
       :tacn:`repeat`, or branching command is aborted and the level is decremented. In
       the case of :n:`+`, a non-zero level skips the first backtrack point, even if
-      the call to :n:`fail @natural` is not enclosed in a :n:`+` command,
+      the call to :n:`fail @num` is not enclosed in a :n:`+` command,
       respecting the algebraic identity.
 
    .. tacv:: fail {* message_token}
 
       The given tokens are used for printing the failure message.
 
-   .. tacv:: fail @natural {* message_token}
+   .. tacv:: fail @num {* message_token}
 
       This is a combination of the previous variants.
 
@@ -573,7 +576,7 @@ Failing
 
    .. tacv:: gfail {* message_token}
 
-   .. tacv:: gfail @natural {* message_token}
+   .. tacv:: gfail @num {* message_token}
 
       These variants fail with an error message or an error level even if
       there are no goals left. Be careful however if Coq terms have to be
@@ -581,7 +584,7 @@ Failing
       tactic into the goals, meaning that if there are no goals when it is
       evaluated, a tactic call like :n:`let x:=H in fail 0 x` will succeed.
 
-   .. exn:: Tactic Failure message (level @natural).
+   .. exn:: Tactic Failure message (level @num).
 
 Timeout
 ~~~~~~~
@@ -760,11 +763,11 @@ We can carry out pattern matching on terms with:
    branches or inside the right-hand side of the selected branch even if it
    has backtracking points.
 
-   .. exn:: No matching clauses for match
+   .. exn:: No matching clauses for match.
 
       No pattern can be used and, in particular, there is no :n:`_` pattern.
 
-   .. exn:: Argument of match does not evaluate to a term
+   .. exn:: Argument of match does not evaluate to a term.
 
       This happens when :n:`@expr` does not denote a term.
 
@@ -844,7 +847,7 @@ We can make pattern matching on goals using the following expression:
    branches or combinations of hypotheses, or inside the right-hand side of
    the selected branch even if it has backtracking points.
 
-   .. exn:: No matching clauses for match goal
+   .. exn:: No matching clauses for match goal.
 
       No clause succeeds, i.e. all matching patterns, if any, fail at the
       application of the right-hand-side.
@@ -891,7 +894,7 @@ produce subgoals but generates a term to be used in tactic expressions:
    match expression. This expression evaluates replaces the hole of the
    value of :n:`@ident` by the value of :n:`@expr`.
 
-   .. exn:: not a context variable
+   .. exn:: Not a context variable.
 
 Generating fresh hypothesis names
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1001,7 +1004,7 @@ Testing boolean expressions
          all:let n:= numgoals in guard n<4.
          Fail all:let n:= numgoals in guard n=2.
 
-   .. exn:: Condition not satisfied
+   .. exn:: Condition not satisfied.
 
 Proving a subgoal as a separate lemma
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1051,8 +1054,8 @@ Proving a subgoal as a separate lemma
          with tactics is fragile, and explicitly named and reused subterms
          don’t play well with asynchronous proofs.
 
-   .. exn:: Proof is not complete
-      :name: Proof is not complete (abstract)
+   .. exn:: Proof is not complete.
+      :name: Proof is not complete. (abstract)
 
 Tactic toplevel definitions
 ---------------------------
@@ -1092,7 +1095,7 @@ Basically, |Ltac| toplevel definitions are made as follows:
 Printing |Ltac| tactics
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Print Ltac @qualid.
+.. cmd:: Print Ltac @qualid
 
    Defined |Ltac| functions can be displayed using this command.
 
@@ -1107,10 +1110,11 @@ Info trace
 ~~~~~~~~~~
 
 .. cmd:: Info @num @expr
+   :name: Info
 
    This command can be used to print the trace of the path eventually taken by an
    |Ltac| script. That is, the list of executed tactics, discarding
-   all the branches which have failed. To that end the Info command can be
+   all the branches which have failed. To that end the :cmd:`Info` command can be
    used with the following syntax.
 
 
@@ -1137,23 +1141,22 @@ Info trace
 
          Info 1 t 1||t 0.
 
-   The trace produced by ``Info`` tries its best to be a reparsable
+   The trace produced by :cmd:`Info` tries its best to be a reparsable
    |Ltac| script, but this goal is not achievable in all generality.
    So some of the output traces will contain oddities.
 
-   As an additional help for debugging, the trace produced by ``Info`` contains
-   (in comments) the messages produced by the idtac
-   tacticals \ `4.2 <#ltac%3Aidtac>`__ at the right possition in the
-   script. In particular, the calls to idtac in branches which failed are
+   As an additional help for debugging, the trace produced by :cmd:`Info` contains
+   (in comments) the messages produced by the :tacn:`idtac` tactical at the right
+   position in the script. In particular, the calls to idtac in branches which failed are
    not printed.
 
-   .. opt:: Info Level @num.
+   .. opt:: Info Level @num
 
-      This option is an alternative to the ``Info`` command.
+      This option is an alternative to the :cmd:`Info` command.
 
       This will automatically print the same trace as :n:`Info @num` at each
       tactic call. The unfolding level can be overridden by a call to the
-      ``Info`` command.
+      :cmd:`Info` command.
 
 Interactive debugger
 ~~~~~~~~~~~~~~~~~~~~
@@ -1223,7 +1226,7 @@ performance bug.
 
    .. warning::
 
-      Backtracking across a Reset Ltac Profile will not restore the information.
+      Backtracking across a :cmd:`Reset Ltac Profile` will not restore the information.
 
 .. coqtop:: reset in
 
@@ -1286,8 +1289,8 @@ performance bug.
    benchmarking purposes.
 
 You can also pass the ``-profile-ltac`` command line option to ``coqc``, which
-performs a ``Set Ltac Profiling`` at the beginning of each document, and a
-``Show Ltac Profile`` at the end.
+turns the :opt:`Ltac Profiling` option on at the beginning of each document,
+and performs a :cmd:`Show Ltac Profile` at the end.
 
 .. warning::
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 86c94bab36..df8ef74f74 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -34,7 +34,7 @@ terms of λ-calculus, known as the *Curry-Howard isomorphism*
 terms are called *proof terms*.
 
 
-.. exn:: No focused proof
+.. exn:: No focused proof.
 
 Coq raises this error message when one attempts to use a proof editing command
 out of the proof editing mode.
@@ -49,7 +49,7 @@ the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
 list of assertion commands is given in Section :ref:`Assertions`. The command
 :cmd:`Goal` can also be used.
 
-.. cmd:: Goal @form.
+.. cmd:: Goal @form
 
 This is intended for quick assertion of statements, without knowing in
 advance which name to give to the assertion, typically for quick
@@ -68,7 +68,7 @@ proof term to the declared name of the original goal. This name is
 added to the environment as an opaque constant.
 
 
-.. exn:: Attempt to save an incomplete proof
+.. exn:: Attempt to save an incomplete proof.
 
 .. note::
 
@@ -81,34 +81,36 @@ proof term is completely rechecked at this point, one may have to wait
 a while when the proof is large. In some exceptional cases one may
 even incur a memory overflow.
 
-.. cmdv:: Defined.
+.. cmdv:: Defined
    :name: Defined (interactive proof)
 
 Defines the proved term as a transparent constant.
 
-.. cmdv:: Save @ident.
+.. cmdv:: Save @ident
 
 Forces the name of the original goal to be :n:`@ident`. This
 command (and the following ones) can only be used if the original goal
 has been opened using the ``Goal`` command.
 
-.. cmd:: Admitted.
+.. cmd:: Admitted
    :name: Admitted (interactive proof)
 
-This command is available in interactive editing proof mode to give up
+This command is available in interactive editing mode to give up
 the current proof and declare the initial goal as an axiom.
 
-.. cmd:: Proof @term.
+.. cmd:: Proof @term
    :name: Proof `term`
 
 This command applies in proof editing mode. It is equivalent to
 
-.. cmd:: exact @term. Qed.
+.. coqtop:: in
+
+   exact @term. Qed.
 
 That is, you have to give the full proof in one gulp, as a
 proof term (see Section :ref:`applyingtheorems`).
 
-.. cmdv:: Proof.
+.. cmdv:: Proof
    :name: Proof (interactive proof)
 
 Is a noop which is useful to delimit the sequence of tactic commands
@@ -121,7 +123,7 @@ See also: ``Proof with tactic.`` in Section
 :ref:`tactics-implicit-automation`.
 
 
-.. cmd:: Proof using @ident1 ... @identn.
+.. cmd:: Proof using @ident1 ... @identn
 
 This command applies in proof editing mode. It declares the set of
 section variables (see :ref:`gallina-assumptions`) used by the proof. At ``Qed`` time, the
@@ -133,23 +135,23 @@ example if ``T`` is variable and a is a variable of type ``T``, the commands
 ``Proof using a`` and ``Proof using T a``` are actually equivalent.
 
 
-.. cmdv:: Proof using @ident1 ... @identn with @tactic.
+.. cmdv:: Proof using @ident1 ... @identn with @tactic
 
 in Section :ref:`tactics-implicit-automation`.
 
-.. cmdv:: Proof using All.
+.. cmdv:: Proof using All
 
 Use all section variables.
 
 
-.. cmdv:: Proof using Type.
+.. cmdv:: Proof using Type
 
-.. cmdv:: Proof using.
+.. cmdv:: Proof using
 
 Use only section variables occurring in the statement.
 
 
-.. cmdv:: Proof using Type*.
+.. cmdv:: Proof using Type*
 
 The ``*`` operator computes the forward transitive closure. E.g. if the
 variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type
@@ -157,21 +159,21 @@ of ``H``. ``Type*`` is the forward transitive closure of the entire set of
 section variables occurring in the statement.
 
 
-.. cmdv:: Proof using -(@ident1 ... @identn).
+.. cmdv:: Proof using -(@ident1 ... @identn)
 
 Use all section variables except :n:`@ident1` ... :n:`@identn`.
 
 
-.. cmdv:: Proof using @collection1 + @collection2 .
+.. cmdv:: Proof using @collection1 + @collection2
 
 
-.. cmdv:: Proof using @collection1 - @collection2 .
+.. cmdv:: Proof using @collection1 - @collection2
 
 
-.. cmdv:: Proof using @collection - ( @ident1 ... @identn ).
+.. cmdv:: Proof using @collection - ( @ident1 ... @identn )
 
 
-.. cmdv:: Proof using @collection * .
+.. cmdv:: Proof using @collection *
 
 Use section variables being, respectively, in the set union, set
 difference, set complement, set forward transitive closure. See
@@ -185,14 +187,14 @@ Proof using options
 The following options modify the behavior of ``Proof using``.
 
 
-.. opt:: Default Proof Using "@expression".
+.. opt:: Default Proof Using "@expression"
 
    Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default
    Proof Using "a b"``. will complete all ``Proof`` commands not followed by a
    using part with using ``a`` ``b``.
 
 
-.. opt:: Suggest Proof Using.
+.. opt:: Suggest Proof Using
 
    When ``Qed`` is performed, suggest a using annotation if the user did not
    provide one.
@@ -232,29 +234,29 @@ Define the collection named "Many" containing the set difference of
 "Fewer" and the unnamed collection ``x`` ``y``
 
 
-.. cmd:: Abort.
+.. cmd:: Abort
 
 This command cancels the current proof development, switching back to
 the previous proof development, or to the |Coq| toplevel if no other
 proof was edited.
 
 
-.. exn:: No focused proof (No proof-editing in progress)
+.. exn:: No focused proof (No proof-editing in progress).
 
 
 
-.. cmdv::  Abort @ident.
+.. cmdv::  Abort @ident
 
 Aborts the editing of the proof named :n:`@ident`.
 
-.. cmdv:: Abort All.
+.. cmdv:: Abort All
 
 Aborts all current goals, switching back to the |Coq|
 toplevel.
 
 
 
-.. cmd:: Existential @num := @term.
+.. cmd:: Existential @num := @term
 
 This command instantiates an existential variable. :n:`@num` is an index in
 the list of uninstantiated existential variables displayed by ``Show
@@ -271,7 +273,7 @@ See also: ``instantiate (num:= term).`` in Section
 See also: ``Grab Existential Variables.`` below.
 
 
-.. cmd:: Grab Existential Variables.
+.. cmd:: Grab Existential Variables
 
 This command can be run when a proof has no more goal to be solved but
 has remaining uninstantiated existential variables. It takes every
@@ -281,84 +283,80 @@ uninstantiated existential variable and turns it into a goal.
 Navigation in the proof tree
 --------------------------------
 
+.. cmd:: Undo
 
-.. cmd:: Undo.
-
-This command cancels the effect of the last command. Thus, it
-backtracks one step.
-
+   This command cancels the effect of the last command. Thus, it
+   backtracks one step.
 
-.. cmdv:: Undo @num.
+.. cmdv:: Undo @num
 
-Repeats Undo :n:`@num` times.
+   Repeats Undo :n:`@num` times.
 
-.. cmdv:: Restart.
+.. cmdv:: Restart
    :name: Restart
 
-This command restores the proof editing process to the original goal.
+   This command restores the proof editing process to the original goal.
 
+   .. exn:: No focused proof to restart.
 
-.. exn:: No focused proof to restart
+.. cmd:: Focus
 
+   This focuses the attention on the first subgoal to prove and the
+   printing of the other subgoals is suspended until the focused subgoal
+   is solved or unfocused. This is useful when there are many current
+   subgoals which clutter your screen.
 
-.. cmd:: Focus.
+.. cmdv:: Focus @num
 
-This focuses the attention on the first subgoal to prove and the
-printing of the other subgoals is suspended until the focused subgoal
-is solved or unfocused. This is useful when there are many current
-subgoals which clutter your screen.
+   This focuses the attention on the :n:`@num` th subgoal to prove.
 
+   .. deprecated:: 8.8
 
-.. cmdv:: Focus @num.
+      Prefer the use of bullets or
+      focusing brackets instead, including :n:`@num : %{`
 
-This focuses the attention on the :n:`@num` th subgoal to
-prove.
+.. cmd:: Unfocus
 
-*This command is deprecated since 8.8*: prefer the use of bullets or
-focusing brackets instead, including :n:`@num : %{`
+   This command restores to focus the goal that were suspended by the
+   last ``Focus`` command.
 
-.. cmd:: Unfocus.
+   .. deprecated:: 8.8
 
-This command restores to focus the goal that were suspended by the
-last ``Focus`` command.
+.. cmd:: Unfocused
 
-*This command is deprecated since 8.8.*
-
-.. cmd:: Unfocused.
-
-Succeeds if the proof is fully unfocused, fails is there are some
-goals out of focus.
+   Succeeds if the proof is fully unfocused, fails if there are some
+   goals out of focus.
 
 .. _curly-braces:
 
 .. cmd:: %{ %| %}
 
-The command ``{`` (without a terminating period) focuses on the first
-goal, much like ``Focus.`` does, however, the subproof can only be
-unfocused when it has been fully solved ( *i.e.* when there is no
-focused goal left). Unfocusing is then handled by ``}`` (again, without a
-terminating period). See also example in next section.
+   The command ``{`` (without a terminating period) focuses on the first
+   goal, much like ``Focus.`` does, however, the subproof can only be
+   unfocused when it has been fully solved ( *i.e.* when there is no
+   focused goal left). Unfocusing is then handled by ``}`` (again, without a
+   terminating period). See also example in next section.
 
-Note that when a focused goal is proved a message is displayed
-together with a suggestion about the right bullet or ``}`` to unfocus it
-or focus the next one.
+   Note that when a focused goal is proved a message is displayed
+   together with a suggestion about the right bullet or ``}`` to unfocus it
+   or focus the next one.
 
 .. cmdv:: @num: %{
 
-This focuses on the :n:`@num` th subgoal to prove.
+   This focuses on the :n:`@num` th subgoal to prove.
 
-Error messages:
+   Error messages:
 
-.. exn:: This proof is focused, but cannot be unfocused this way
+   .. exn:: This proof is focused, but cannot be unfocused this way.
 
-You are trying to use ``}`` but the current subproof has not been fully solved.
+      You are trying to use ``}`` but the current subproof has not been fully solved.
 
-.. exn:: No such goal
-   :name: No such goal (focusing)
+   .. exn:: No such goal.
+      :name: No such goal. (Focusing)
 
-.. exn:: Brackets only support the single numbered goal selector
+   .. exn:: Brackets only support the single numbered goal selector.
 
-See also error messages about bullets below.
+      See also error messages about bullets below.
 
 .. _bullets:
 
@@ -409,11 +407,11 @@ The following example script illustrates all these features:
     assumption.
 
 
-.. exn:: Wrong bullet @bullet1 : Current bullet @bullet2 is not finished.
+.. exn:: Wrong bullet @bullet1: Current bullet @bullet2 is not finished.
 
 Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same.
 
-.. exn:: Wrong bullet @bullet1 : Bullet @bullet2 is mandatory here.
+.. exn:: Wrong bullet @bullet1: Bullet @bullet2 is mandatory here.
 
 You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here.
 
@@ -427,17 +425,12 @@ You just finished a goal focused by ``{``, you must unfocus it with ``}``.
 
 Set Bullet Behavior
 ```````````````````
+.. opt:: Bullet Behavior  %( "None" %| "Strict Subproofs" %)
 
-The bullet behavior can be controlled by the following commands.
-
-.. opt:: Bullet Behavior "None"
-
-This makes bullets inactive.
-
-.. opt:: Bullet Behavior "Strict Subproofs"
-
-This makes bullets active (this is the default behavior).
+   This option controls the bullet behavior and can take two possible values:
 
+   - "None": this makes bullets inactive.
+   - "Strict Subproofs": this makes bullets active (this is the default behavior).
 
 .. _requestinginformation:
 
@@ -445,7 +438,7 @@ Requesting information
 ----------------------
 
 
-.. cmd:: Show.
+.. cmd:: Show
 
 This command displays the current goals.
 
@@ -454,10 +447,10 @@ This command displays the current goals.
 
 Displays only the :n:`@num`-th subgoal.
 
-.. exn:: No such goal
-.. exn:: No focused proof
+.. exn:: No such goal.
+.. exn:: No focused proof.
 
-.. cmdv:: Show @ident.
+.. cmdv:: Show @ident
 
 Displays the named goal :n:`@ident`. This is useful in
 particular to display a shelved goal but only works if the
@@ -472,7 +465,7 @@ corresponding existential variable has been named by the user
     eexists ?[n].
     Show n.
 
-.. cmdv:: Show Script.
+.. cmdv:: Show Script
 
 Displays the whole list of tactics applied from the
 beginning of the current proof. This tactics script may contain some
@@ -480,7 +473,7 @@ holes (subgoals not yet proved). They are printed under the form
 
 ``<Your Tactic Text here>``.
 
-.. cmdv:: Show Proof.
+.. cmdv:: Show Proof
 
 It displays the proof term generated by the tactics
 that have been applied. If the proof is not completed, this term
@@ -490,14 +483,14 @@ integer, and applied to the list of variables in the context, since it
 may depend on them. The types obtained by abstracting away the context
 from the type of each hole-placer are also printed.
 
-.. cmdv:: Show Conjectures.
+.. cmdv:: Show Conjectures
 
 It prints the list of the names of all the
 theorems that are currently being proved. As it is possible to start
 proving a previous lemma during the proof of a theorem, this list may
 contain several names.
 
-.. cmdv:: Show Intro.
+.. cmdv:: Show Intro
 
 If the current goal begins by at least one product,
 this command prints the name of the first product, as it would be
@@ -507,18 +500,18 @@ Proof General macro, it is possible to transform any anonymous ``intro``
 into a qualified one such as ``intro y13``. In the case of a non-product
 goal, it prints nothing.
 
-.. cmdv:: Show Intros.
+.. cmdv:: Show Intros
 
 This command is similar to the previous one, it
 simulates the naming process of an intros.
 
-.. cmdv:: Show Existentials.
+.. cmdv:: Show Existentials
 
 It displays the set of all uninstantiated
 existential variables in the current proof tree, along with the type
 and the context of each variable.
 
-.. cmdv:: Show Match @ident.
+.. cmdv:: Show Match @ident
 
 This variant displays a template of the Gallina
 ``match`` construct with a branch for each constructor of the type
@@ -529,26 +522,26 @@ This variant displays a template of the Gallina
 
      Show Match nat.
 
-.. exn:: Unknown inductive type
+.. exn:: Unknown inductive type.
 
 .. _ShowUniverses:
 
-.. cmdv:: Show Universes.
+.. cmdv:: Show Universes
 
 It displays the set of all universe constraints and
 its normalized form at the current stage of the proof, useful for
 debugging universe inconsistencies.
 
 
-.. cmd:: Guarded.
+.. cmd:: Guarded
 
-Some tactics (e.g. :tacn:`refine` :ref:`applyingtheorems`) allow to build proofs using
+Some tactics (e.g. :tacn:`refine`) allow to build proofs using
 fixpoint or co-fixpoint constructions. Due to the incremental nature
 of interactive proof construction, the check of the termination (or
 guardedness) of the recursive calls in the fixpoint or cofixpoint
 constructions is postponed to the time of the completion of the proof.
 
-The command ``Guarded`` allows checking if the guard condition for
+The command :cmd:`Guarded` allows checking if the guard condition for
 fixpoint and cofixpoint is violated at some time of the construction
 of the proof without having to wait the completion of the proof.
 
@@ -570,13 +563,12 @@ available hypotheses.
 
 This option controls the way binders are handled
 in assertion commands such as ``Theorem ident [binders] : form``. When the
-option is set, which is the default, binders are automatically put in
+option is on, which is the default, binders are automatically put in
 the local context of the goal to prove.
 
-The option can be unset by issuing ``Unset Automatic Introduction``. When
-the option is unset, binders are discharged on the statement to be
-proved and a tactic such as intro (see Section :ref:`managingthelocalcontext`) has to be
-used to move the assumptions to the local context.
+When the option is off, binders are discharged on the statement to be
+proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
+has to be used to move the assumptions to the local context.
 
 
 Controlling memory usage
@@ -586,15 +578,15 @@ When experiencing high memory usage the following commands can be used
 to force |Coq| to optimize some of its internal data structures.
 
 
-.. cmd:: Optimize Proof.
+.. cmd:: Optimize Proof
 
 This command forces |Coq| to shrink the data structure used to represent
 the ongoing proof.
 
 
-.. cmd:: Optimize Heap.
+.. cmd:: Optimize Heap
 
 This command forces the |OCaml| runtime to perform a heap compaction.
 This is in general an expensive operation.
 See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-There is also an analogous tactic :tac:`optimize_heap`.
+There is also an analogous tactic :tacn:`optimize_heap`.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 977a5b8fad..63cd0f3ead 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -423,7 +423,7 @@ an improvement over ``all null s``.
 
 The syntax of the new declaration is
 
-.. cmd:: Prenex Implicits {+ @ident}.
+.. cmd:: Prenex Implicits {+ @ident}
 
 Let us denote :math:`c_1` … :math:`c_n` the list of identifiers given to a
 ``Prenex Implicits`` command.  The command checks that each ci is the name of
@@ -2157,10 +2157,10 @@ equivalent to:
 
 More generally, the tactic:
 
-.. tacn:: @tactic; last @natural first
+.. tacn:: @tactic; last @num first
    :name: last first
 
-where :token:`natural` is a |Coq| numeral, or and Ltac variable
+where :token:`num` is a |Coq| numeral, or an Ltac variable
 denoting a |Coq|
 numeral, having the value k. It rotates the n subgoals G1 , …, Gn
 generated by tactic. The first subgoal becomes Gn + 1 − k and the
@@ -2168,7 +2168,7 @@ circular order of subgoals remains unchanged.
 
 Conversely, the tactic:
 
-.. tacn:: @tactic; first @natural last
+.. tacn:: @tactic; first @num last
    :name: first last
 
 rotates the n subgoals G1 , …, Gn generated by tactic in order that
@@ -5322,11 +5322,11 @@ intro item  see :ref:`introduction_ssr`
 
 multiplier  see :ref:`iteration_ssr`
 
-.. prodn:: occ_switch ::= { {? + %| - } {* @natural } }
+.. prodn:: occ_switch ::= { {? + %| - } {* @num } }
 
 occur. switch see :ref:`occurrence_selection_ssr`
 
-.. prodn:: mult ::= {? @natural } @mult_mark
+.. prodn:: mult ::= {? @num } @mult_mark
 
 multiplier see :ref:`iteration_ssr`
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6c1b1c08c1..b3537bad80 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -92,7 +92,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
   the ``n``-th non dependent premise of the ``term``, as determined by the type
   of ``term``.
 
-  .. exn:: No such binder
+  .. exn:: No such binder.
 
 + A bindings list can also be a simple list of terms :n:`{* term}`.
   In that case the references to which these terms correspond are
@@ -151,8 +151,8 @@ no numbers are given, all occurrences of :n:`@term` in the goal are selected.
 Finally, the last notation is an abbreviation for ``* |- *``. Note also
 that ``|-`` is optional in the first case when no ``*`` is given.
 
-Here are some tactics that understand occurrences clauses: ``set``, ``remember``
-, ``induction``, ``destruct``.
+Here are some tactics that understand occurrences clauses: :tacn:`set`, :tacn:`remember`
+, :tacn:`induction`, :tacn:`destruct`.
 
 
 See also: :ref:`Managingthelocalcontext`,
@@ -167,201 +167,203 @@ Applying theorems
 .. tacn:: exact @term
    :name: exact
 
-This tactic applies to any goal. It gives directly the exact proof
-term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then
-``exact p`` succeeds iff ``T`` and ``U`` are convertible (see
-:ref:`Conversion-rules`).
+   This tactic applies to any goal. It gives directly the exact proof
+   term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then
+   ``exact p`` succeeds iff ``T`` and ``U`` are convertible (see
+   :ref:`Conversion-rules`).
 
-.. exn:: Not an exact proof.
+   .. exn:: Not an exact proof.
 
-.. tacv:: eexact @term.
-   :name: eexact
+   .. tacv:: eexact @term.
+      :name: eexact
 
-This tactic behaves like exact but is able to handle terms and goals with
-meta-variables.
+      This tactic behaves like exact but is able to handle terms and goals with
+      meta-variables.
 
 .. tacn:: assumption
    :name: assumption
 
-This tactic looks in the local context for an hypothesis which type is equal to
-the goal. If it is the case, the subgoal is proved. Otherwise, it fails.
+   This tactic looks in the local context for an hypothesis which type is equal to
+   the goal. If it is the case, the subgoal is proved. Otherwise, it fails.
 
-.. exn:: No such assumption.
+   .. exn:: No such assumption.
 
-.. tacv:: eassumption
-   :name: eassumption
+   .. tacv:: eassumption
+      :name: eassumption
 
-This tactic behaves like assumption but is able to handle goals with
-meta-variables.
+      This tactic behaves like assumption but is able to handle goals with
+      meta-variables.
 
 .. tacn:: refine @term
    :name: refine
 
-This tactic applies to any goal. It behaves like exact with a big
-difference: the user can leave some holes (denoted by ``_`` or``(_:type)``) in
-the term. refine will generate as many subgoals as there are holes in
-the term. The type of holes must be either synthesized by the system
-or declared by an explicit cast like ``(_:nat->Prop)``. Any subgoal that
-occurs in other subgoals is automatically shelved, as if calling
-shelve_unifiable (see Section 8.17.4). This low-level tactic can be
-useful to advanced users.
+   This tactic applies to any goal. It behaves like :tacn:`exact` with a big
+   difference: the user can leave some holes (denoted by ``_`` or ``(_:type)``) in
+   the term. :tacn:`refine` will generate as many subgoals as there are holes in
+   the term. The type of holes must be either synthesized by the system
+   or declared by an explicit cast like ``(_:nat->Prop)``. Any subgoal that
+   occurs in other subgoals is automatically shelved, as if calling
+   :tacn:`shelve_unifiable`. This low-level tactic can be
+   useful to advanced users.
 
-.. example::
-  .. coqtop:: reset all
+   .. example::
+      .. coqtop:: reset all
 
-     Inductive Option : Set :=
-     | Fail : Option
-     | Ok : bool -> Option.
+         Inductive Option : Set :=
+         | Fail : Option
+         | Ok : bool -> Option.
 
-     Definition get : forall x:Option, x <> Fail -> bool.
+         Definition get : forall x:Option, x <> Fail -> bool.
 
-     refine
-       (fun x:Option =>
-          match x return x <> Fail -> bool with
-          | Fail => _
-          | Ok b => fun _ => b
-          end).
+         refine
+           (fun x:Option =>
+           match x return x <> Fail -> bool with
+           | Fail => _
+           | Ok b => fun _ => b
+           end).
 
-     intros; absurd (Fail = Fail); trivial.
+         intros; absurd (Fail = Fail); trivial.
 
-     Defined.
+         Defined.
 
-.. exn:: invalid argument
+   .. exn:: Invalid argument.
 
-   The tactic ``refine`` does not know what to do with the term you gave.
+      The tactic :tacn:`refine` does not know what to do with the term you gave.
 
-.. exn:: Refine passed ill-formed term
+   .. exn:: Refine passed ill-formed term.
 
-   The term you gave is not a valid proof (not easy to debug in general). This
-   message may also occur in higher-level tactics that call ``refine``
-   internally.
+      The term you gave is not a valid proof (not easy to debug in general). This
+      message may also occur in higher-level tactics that call :tacn:`refine`
+      internally.
 
-.. exn:: Cannot infer a term for this placeholder
+   .. exn:: Cannot infer a term for this placeholder.
+      :name: Cannot infer a term for this placeholder. (refine)
 
-   There is a hole in the term you gave which type cannot be inferred. Put a
-   cast around it.
+      There is a hole in the term you gave whose type cannot be inferred. Put a
+      cast around it.
 
-.. tacv:: simple refine @term
-   :name: simple refine
+   .. tacv:: simple refine @term
+      :name: simple refine
 
-   This tactic behaves like refine, but it does not shelve any subgoal. It does
-   not perform any beta-reduction either.
+      This tactic behaves like refine, but it does not shelve any subgoal. It does
+      not perform any beta-reduction either.
 
-.. tacv:: notypeclasses refine @term
+   .. tacv:: notypeclasses refine @term
+      :name: notypeclasses refine
 
-   This tactic behaves like ``refine`` except it performs typechecking without
-   resolution of typeclasses.
+      This tactic behaves like :tacn:`refine` except it performs typechecking without
+      resolution of typeclasses.
 
-.. tacv:: simple notypeclasses refine @term
-   :name: simple notypeclasses refine
+   .. tacv:: simple notypeclasses refine @term
+      :name: simple notypeclasses refine
 
-   This tactic behaves like ``simple refine`` except it performs typechecking
-   without resolution of typeclasses.
+      This tactic behaves like :tacn:`simple refine` except it performs typechecking
+      without resolution of typeclasses.
 
-.. tacv:: apply @term
+.. tacn:: apply @term
    :name: apply
 
-This tactic applies to any goal. The argument term is a term well-formed in the
-local context. The tactic apply tries to match the current goal against the
-conclusion of the type of term. If it succeeds, then the tactic returns as many
-subgoals as the number of non-dependent premises of the type of term. If the
-conclusion of the type of term does not match the goal *and* the conclusion is
-an inductive type isomorphic to a tuple type, then each component of the tuple
-is recursively matched to the goal in the left-to-right order.
+   This tactic applies to any goal. The argument term is a term well-formed in the
+   local context. The tactic apply tries to match the current goal against the
+   conclusion of the type of term. If it succeeds, then the tactic returns as many
+   subgoals as the number of non-dependent premises of the type of term. If the
+   conclusion of the type of term does not match the goal *and* the conclusion is
+   an inductive type isomorphic to a tuple type, then each component of the tuple
+   is recursively matched to the goal in the left-to-right order.
 
-The tactic ``apply`` relies on first-order unification with dependent types
-unless the conclusion of the type of ``term`` is of the form :g:`P (t`:sub:`1`
-:g:`...` :g:`t`:sub:`n` :g:`)` with `P` to be instantiated. In the latter case, the behavior
-depends on the form of the goal. If the goal is of the form
-:g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n` and the :g:`t`:sub:`i` and
-:g:`u`:sub:`i` unifies, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise,
-``apply`` tries to define :g:`P` by abstracting over :g:`t`:sub:`1`  :g:`...`
-:g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it
-gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...`  :g:`u`:sub:`n`.
+   The tactic :tacn:`apply` relies on first-order unification with dependent types
+   unless the conclusion of the type of :token:`term` is of the form :g:`P (t`:sub:`1`
+   :g:`...` :g:`t`:sub:`n` :g:`)` with `P` to be instantiated. In the latter case, the behavior
+   depends on the form of the goal. If the goal is of the form
+   :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n` and the :g:`t`:sub:`i` and
+   :g:`u`:sub:`i` unifies, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise,
+   :tacn:`apply` tries to define :g:`P` by abstracting over :g:`t`:sub:`1`  :g:`...`
+   :g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it
+   gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...`  :g:`u`:sub:`n`.
 
-.. exn:: Unable to unify ... with ... .
+   .. exn:: Unable to unify ... with ... .
 
-The apply tactic failed to match the conclusion of term and the current goal.
-You can help the apply tactic by transforming your goal with the
-:tacn:`change` or :tacn:`pattern` tactics.
+      The apply tactic failed to match the conclusion of :token:`term` and the
+      current goal. You can help the apply tactic by transforming your goal with
+      the :tacn:`change` or :tacn:`pattern` tactics.
 
-.. exn:: Unable to find an instance for the variables {+ @ident}.
+   .. exn:: Unable to find an instance for the variables {+ @ident}.
 
-This occurs when some instantiations of the premises of term are not deducible
-from the unification. This is the case, for instance, when you want to apply a
-transitivity property. In this case, you have to use one of the variants below:
+      This occurs when some instantiations of the premises of :token:`term` are not deducible
+      from the unification. This is the case, for instance, when you want to apply a
+      transitivity property. In this case, you have to use one of the variants below:
 
-.. tacv:: apply @term with {+ @term}
+   .. tacv:: apply @term with {+ @term}
 
-Provides apply with explicit instantiations for all dependent premises of the
-type of term that do not occur in the conclusion and consequently cannot be
-found by unification. Notice that the collection :n:`{+ @term}` must be given
-according to the order of these dependent premises of the type of term.
+      Provides apply with explicit instantiations for all dependent premises of the
+      type of term that do not occur in the conclusion and consequently cannot be
+      found by unification. Notice that the collection :n:`{+ @term}` must be given
+      according to the order of these dependent premises of the type of term.
 
-.. exn:: Not the right number of missing arguments.
+      .. exn:: Not the right number of missing arguments.
 
-.. tacv:: apply @term with @bindings_list
+   .. tacv:: apply @term with @bindings_list
 
-This also provides apply with values for instantiating premises. Here, variables
-are referred by names and non-dependent products by increasing numbers (see
-:ref:`bindings list <bindingslist>`).
+      This also provides apply with values for instantiating premises. Here, variables
+      are referred by names and non-dependent products by increasing numbers (see
+      :ref:`bindings list <bindingslist>`).
 
-.. tacv:: apply {+, @term}
+   .. tacv:: apply {+, @term}
 
-This is a shortcut for ``apply term``:sub:`1`
-``; [.. | ... ; [ .. | apply`` ``term``:sub:`n` ``] ... ]``,
-i.e. for the successive applications of ``term``:sub:`i+1` on the last subgoal
-generated by ``apply term``:sub:`i` , starting from the application of
-``term``:sub:`1`.
+      This is a shortcut for :n:`apply @term`:sub:`1`
+      :n:`; [.. | ... ; [ .. | apply @term`:sub:`n` :n:`] ... ]`,
+      i.e. for the successive applications of :token:`term`:sub:`i+1` on the last subgoal
+      generated by :n:`apply @term`:sub:`i` , starting from the application of
+      :token:`term`:sub:`1`.
 
-.. tacv:: eapply @term
-   :name: eapply
+   .. tacv:: eapply @term
+      :name: eapply
 
-The tactic ``eapply`` behaves like ``apply`` but it does not fail when no
-instantiations are deducible for some variables in the premises. Rather, it
-turns these variables into existential variables which are variables still to
-instantiate (see :ref:`Existential-Variables`). The instantiation is
-intended to be found later in the proof.
+      The tactic :tacn:`eapply` behaves like :tacn:`apply` but it does not fail when no
+      instantiations are deducible for some variables in the premises. Rather, it
+      turns these variables into existential variables which are variables still to
+      instantiate (see :ref:`Existential-Variables`). The instantiation is
+      intended to be found later in the proof.
 
-.. tacv:: simple apply @term.
-   :name: simple apply
+   .. tacv:: simple apply @term.
+      :name: simple apply
 
-This behaves like ``apply`` but it reasons modulo conversion only on subterms
-that contain no variables to instantiate. For instance, the following example
-does not succeed because it would require the conversion of ``id ?foo`` and
-``O``.
+      This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms
+      that contain no variables to instantiate. For instance, the following example
+      does not succeed because it would require the conversion of ``id ?foo`` and
+      :g:`O`.
 
-.. example::
+      .. example::
 
-   .. coqtop:: all
+         .. coqtop:: all
 
-      Definition id (x : nat) := x.
-      Hypothesis H : forall y, id y = y.
-      Goal O = O.
-      Fail simple apply H.
+            Definition id (x : nat) := x.
+            Parameter H : forall y, id y = y.
+            Goal O = O.
+            Fail simple apply H.
 
-Because it reasons modulo a limited amount of conversion, ``simple apply`` fails
-quicker than ``apply`` and it is then well-suited for uses in user-defined
-tactics that backtrack often. Moreover, it does not traverse tuples as ``apply``
-does.
+      Because it reasons modulo a limited amount of conversion, :tacn:`simple apply` fails
+      quicker than :tacn:`apply` and it is then well-suited for uses in user-defined
+      tactics that backtrack often. Moreover, it does not traverse tuples as :tacn:`apply`
+      does.
 
-.. tacv:: {? simple} apply {+, @term {? with @bindings_list}}
-.. tacv:: {? simple} eapply {+, @term {? with @bindings_list}}
-   :name: simple eapply
+   .. tacv:: {? simple} apply {+, @term {? with @bindings_list}}
+   .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}}
+      :name: simple eapply
 
-This summarizes the different syntaxes for ``apply`` and ``eapply``.
+      This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`.
 
-.. tacv:: lapply @term
-   :name: lapply
+   .. tacv:: lapply @term
+      :name: lapply
 
-This tactic applies to any goal, say :g:`G`. The argument term has to be
-well-formed in the current context, its type being reducible to a non-dependent
-product :g:`A -> B` with :g:`B` possibly containing products. Then it generates
-two subgoals :g:`B->G` and :g:`A`. Applying ``lapply H`` (where :g:`H` has type
-:g:`A->B` and :g:`B` does not start with a product) does the same as giving the
-sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
+      This tactic applies to any goal, say :g:`G`. The argument term has to be
+      well-formed in the current context, its type being reducible to a non-dependent
+      product :g:`A -> B` with :g:`B` possibly containing products. Then it generates
+      two subgoals :g:`B->G` and :g:`A`. Applying ``lapply H`` (where :g:`H` has type
+      :g:`A->B` and :g:`B` does not start with a product) does the same as giving the
+      sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
 
-.. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product.
+      .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product.
 
 .. example::
    Assume we have a transitive relation ``R`` on ``nat``:
@@ -528,8 +530,8 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    constructor of :g:`I`, then ``constructor i`` is equivalent to
    ``intros; apply c``:sub:`i`.
 
-.. exn:: Not an inductive product
-.. exn:: Not enough constructors
+.. exn:: Not an inductive product.
+.. exn:: Not enough constructors.
 
 .. tacv:: constructor
 
@@ -562,7 +564,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    to :n:`intros; constructor 1 with @bindings_list.` It is typically used in
    the case of an existential quantification :math:`\exists`:g:`x, P(x).`
 
-.. exn:: Not an inductive goal with 1 constructor
+.. exn:: Not an inductive goal with 1 constructor.
 
 .. tacv:: exists @bindings_list
 
@@ -579,7 +581,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    Then, they are respectively equivalent to ``constructor 1`` and
    ``constructor 2``.
 
-.. exn:: Not an inductive goal with 2 constructors
+.. exn:: Not an inductive goal with 2 constructors.
 
 .. tacv:: left with @bindings_list
 .. tacv:: right with @bindings_list
@@ -656,7 +658,7 @@ be applied or the goal is not head-reducible.
    This applies ``intro`` but forces :n:`@ident` to be the name of the
    introduced hypothesis.
 
-.. exn:: name @ident is already used
+.. exn:: Name @ident is already used.
 
 .. note:: If a name used by intro hides the base name of a global
    constant then the latter can still be referred to by a qualified name
@@ -675,7 +677,7 @@ be applied or the goal is not head-reducible.
    `(@ident:term)` and discharges the variable named `ident` of the current
    goal.
 
-.. exn:: No such hypothesis in current goal
+.. exn:: No such hypothesis in current goal.
 
 .. tacv:: intros until @num
 
@@ -704,7 +706,7 @@ be applied or the goal is not head-reducible.
    too so as to respect the order of dependencies between hypotheses.
    Note that :n:`intro at bottom` is a synonym for :n:`intro` with no argument.
 
-.. exn:: No such hypothesis : @ident.
+.. exn:: No such hypothesis: @ident.
 
 .. tacv:: intro @ident after @ident
 .. tacv:: intro @ident before @ident
@@ -883,7 +885,7 @@ quantification or an implication.
    This tactic expects :n:`@ident` to be a local definition then clears its
    body. Otherwise said, this tactic turns a definition into an assumption.
 
-.. exn:: @ident is not a local definition
+.. exn:: @ident is not a local definition.
 
 .. tacv:: clear - {+ @ident}
 
@@ -950,9 +952,9 @@ the inverse of :tacn:`intro`.
    This moves ident at the bottom of the local context (at the end of the
    context).
 
-.. exn:: No such hypothesis
-.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident
-.. exn:: Cannot move @ident after @ident : it depends on @ident
+.. exn:: No such hypothesis.
+.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident.
+.. exn:: Cannot move @ident after @ident : it depends on @ident.
 
 .. example::
    .. coqtop:: all
@@ -979,8 +981,8 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    particular, the target identifiers may contain identifiers that exist in the
    source context, as long as the latter are also renamed by the same tactic.
 
-.. exn:: No such hypothesis
-.. exn:: @ident is already used
+.. exn:: No such hypothesis.
+.. exn:: @ident is already used.
 
 .. tacn:: set (@ident := @term)
    :name: set
@@ -992,7 +994,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    first checks that all subterms matching the pattern are compatible before
    doing the replacement using the leftmost subterm matching the pattern.
 
-.. exn:: The variable @ident is already defined
+.. exn:: The variable @ident is already defined.
 
 .. tacv:: set (@ident := @term ) in @goal_occurrences
 
@@ -1110,7 +1112,7 @@ Controlling the proof flow
    :g:`U` [2]_. The subgoal :g:`U` comes first in the list of subgoals remaining to
    prove.
 
-.. exn:: Not a proposition or a type
+.. exn:: Not a proposition or a type.
 
    Arises when the argument form is neither of type :g:`Prop`, :g:`Set` nor
    :g:`Type`.
@@ -1125,8 +1127,8 @@ Controlling the proof flow
    This tactic behaves like :n:`assert` but applies tactic to solve the subgoals
    generated by assert.
 
-   .. exn:: Proof is not complete
-      :name: Proof is not complete (assert)
+   .. exn:: Proof is not complete.
+      :name: Proof is not complete. (assert)
 
 .. tacv:: assert form as intro_pattern
 
@@ -1147,7 +1149,7 @@ Controlling the proof flow
    the type of :g:`term`. This is deprecated in favor of :n:`pose proof`. If the
    head of term is :n:`@ident`, the tactic behaves as :n:`specialize @term`.
 
-   .. exn:: Variable @ident is already declared
+   .. exn:: Variable @ident is already declared.
 
 .. tacv:: eassert form as intro_pattern by tactic
    :name: eassert
@@ -1239,8 +1241,8 @@ Controlling the proof flow
    the goal. The :n:`as` clause is especially useful in this case to immediately
    introduce the instantiated statement as a local hypothesis.
 
-   .. exn:: @ident is used in hypothesis @ident
-   .. exn:: @ident is used in conclusion
+   .. exn:: @ident is used in hypothesis @ident.
+   .. exn:: @ident is used in conclusion.
 
 .. tacn:: generalize @term
    :name: generalize
@@ -1364,7 +1366,7 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`.
    a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory
    hypotheses.
 
-.. exn:: No such assumption
+.. exn:: No such assumption.
 
 .. tacv:: contradiction @ident
 
@@ -1570,9 +1572,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       intros n H.
       induction n.
 
-.. exn:: Not an inductive product
+.. exn:: Not an inductive product.
 
-.. exn:: Unable to find an instance for the variables @ident ... @ident
+.. exn:: Unable to find an instance for the variables @ident ... @ident.
 
    Use in this case the variant :tacn:`elim ... with` below.
 
@@ -1846,8 +1848,8 @@ See also: :ref:`advanced-recursive-functions`
   :ref:`functional-scheme`
   :tacn:`inversion`
 
-.. exn:: Cannot find induction information on @qualid
-.. exn:: Not the right number of induction arguments
+.. exn:: Cannot find induction information on @qualid.
+.. exn:: Not the right number of induction arguments.
 
 .. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list
 
@@ -1880,8 +1882,8 @@ See also: :ref:`advanced-recursive-functions`
    :n:`@ident` is first introduced in the local context using
    :n:`intros until @ident`.
 
-.. exn:: No primitive equality found
-.. exn:: Not a discriminable equality
+.. exn:: No primitive equality found.
+.. exn:: Not a discriminable equality.
 
 .. tacv:: discriminate @num
 
@@ -1909,7 +1911,7 @@ See also: :ref:`advanced-recursive-functions`
    the form :n:`@term <> @term`, this behaves as
    :n:`intro @ident; discriminate @ident`.
 
-   .. exn:: No discriminable equalities
+   .. exn:: No discriminable equalities.
 
 .. tacn:: injection @term
    :name: injection
@@ -1920,7 +1922,7 @@ See also: :ref:`advanced-recursive-functions`
    :g:`t`:sub:`1` and :g:`t`:sub:`2` are equal too.
 
    If :n:`@term` is a proof of a statement of conclusion :n:`@term = @term`,
-   then ``injection`` applies the injectivity of constructors as deep as
+   then :tacn:`injection` applies the injectivity of constructors as deep as
    possible to derive the equality of all the subterms of :n:`@term` and
    :n:`@term` at positions where the terms start to differ. For example, from
    :g:`(S p, S n) = (q, S (S m))` we may derive :g:`S p = q` and
@@ -1930,93 +1932,96 @@ See also: :ref:`advanced-recursive-functions`
    equality of all the subterms at positions where they differ and adds them as
    antecedents to the conclusion of the current goal.
 
-.. example::
+   .. example::
 
-   Consider the following goal:
+      Consider the following goal:
 
-   .. coqtop:: reset all
+      .. coqtop:: in
 
-      Inductive list : Set :=
-      | nil : list
-      | cons : nat -> list -> list.
-      Variable P : list -> Prop.
-      Goal forall l n, P nil -> cons n l = cons 0 nil -> P l.
-      intros.
-      injection H0.
+         Inductive list : Set :=
+         | nil : list
+         | cons : nat -> list -> list.
+         Parameter P : list -> Prop.
+         Goal forall l n, P nil -> cons n l = cons 0 nil -> P l.
 
+      .. coqtop:: all
 
-Beware that injection yields an equality in a sigma type whenever the
-injected object has a dependent type :g:`P` with its two instances in
-different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and
-:g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and
-:g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable
-equality has been declared using the command ``Scheme Equality`` (see :ref:`proofschemes-induction-principles`),
-the use of a sigma type is avoided.
+         intros.
+         injection H0.
 
-.. note::
-   If some quantified hypothesis of the goal is named :n:`@ident`,
-   then :n:`injection @ident` first introduces the hypothesis in the local
-   context using :n:`intros until @ident`.
+   Beware that injection yields an equality in a sigma type whenever the
+   injected object has a dependent type :g:`P` with its two instances in
+   different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and
+   :g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and
+   :g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable
+   equality has been declared using the command :cmd:`Scheme Equality`
+   (see :ref:`proofschemes-induction-principles`),
+   the use of a sigma type is avoided.
 
-.. exn:: Not a projectable equality but a discriminable one
-.. exn:: Nothing to do, it is an equality between convertible @terms
-.. exn:: Not a primitive equality
-.. exn:: Nothing to inject
+   .. note::
+      If some quantified hypothesis of the goal is named :n:`@ident`,
+      then :n:`injection @ident` first introduces the hypothesis in the local
+      context using :n:`intros until @ident`.
 
-.. tacv:: injection @num
+   .. exn:: Not a projectable equality but a discriminable one.
+   .. exn:: Nothing to do, it is an equality between convertible @terms.
+   .. exn:: Not a primitive equality.
+   .. exn:: Nothing to inject.
 
-   This does the same thing as :n:`intros until @num` followed by
-   :n:`injection @ident` where :n:`@ident` is the identifier for the last
-   introduced hypothesis.
+   .. tacv:: injection @num
 
-.. tacv:: injection @term with @bindings_list
+      This does the same thing as :n:`intros until @num` followed by
+      :n:`injection @ident` where :n:`@ident` is the identifier for the last
+      introduced hypothesis.
 
-   This does the same as :n:`injection @term` but using the given bindings to
-   instantiate parameters or hypotheses of :n:`@term`.
+   .. tacv:: injection @term with @bindings_list
 
-.. tacv:: einjection @num
-.. tacv:: einjection @term {? with @bindings_list}
-   :name: einjection
+      This does the same as :n:`injection @term` but using the given bindings to
+      instantiate parameters or hypotheses of :n:`@term`.
 
-   This works the same as :n:`injection` but if the type of :n:`@term`, or the
-   type of the hypothesis referred to by :n:`@num`, has uninstantiated
-   parameters, these parameters are left as existential variables.
+   .. tacv:: einjection @num
+      :name: einjection
+   .. tacv:: einjection @term {? with @bindings_list}
+
+      This works the same as :n:`injection` but if the type of :n:`@term`, or the
+      type of the hypothesis referred to by :n:`@num`, has uninstantiated
+      parameters, these parameters are left as existential variables.
 
-.. tacv:: injection
+   .. tacv:: injection
 
-   If the current goal is of the form :n:`@term <> @term` , this behaves as
-   :n:`intro @ident; injection @ident`.
+      If the current goal is of the form :n:`@term <> @term` , this behaves as
+      :n:`intro @ident; injection @ident`.
 
-   .. exn:: goal does not satisfy the expected preconditions
+      .. exn:: goal does not satisfy the expected preconditions.
 
-.. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern}
-.. tacv:: injection @num as {+ intro_pattern}
-.. tacv:: injection as {+ intro_pattern}
-.. tacv:: einjection @term {? with @bindings_list} as {+ intro_pattern}
-.. tacv:: einjection @num as {+ intro_pattern}
-.. tacv:: einjection as {+ intro_pattern}
+   .. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern}
+   .. tacv:: injection @num as {+ intro_pattern}
+   .. tacv:: injection as {+ intro_pattern}
+   .. tacv:: einjection @term {? with @bindings_list} as {+ intro_pattern}
+   .. tacv:: einjection @num as {+ intro_pattern}
+   .. tacv:: einjection as {+ intro_pattern}
 
    These variants apply :n:`intros {+ @intro_pattern}` after the call to
-   ``injection`` or ``einjection`` so that all equalities generated are moved in
+   :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in
    the context of hypotheses. The number of :n:`@intro_pattern` must not exceed
    the number of equalities newly generated. If it is smaller, fresh
    names are automatically generated to adjust the list of :n:`@intro_pattern`
    to the number of new equalities. The original equality is erased if it
    corresponds to an hypothesis.
 
-.. opt:: Structural Injection
+   .. opt:: Structural Injection
 
-   This option ensure that :n:`injection @term` erases the original hypothesis
-   and leaves the generated equalities in the context rather than putting them
-   as antecedents of the current goal, as if giving :n:`injection @term as`
-   (with an empty list of names). This option is off by default.
+      This option ensure that :n:`injection @term` erases the original hypothesis
+      and leaves the generated equalities in the context rather than putting them
+      as antecedents of the current goal, as if giving :n:`injection @term as`
+      (with an empty list of names). This option is off by default.
 
-.. opt:: Keep Proof Equalities
+   .. opt:: Keep Proof Equalities
 
-   By default, :tacn:`injection` only creates new equalities between :n:`@terms`
-   whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special
-   behavior for objects that are proofs of a statement in :g:`Prop`. This option
-   controls this behavior.
+      By default, :tacn:`injection` only creates new equalities between :n:`@terms`
+      whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special
+      behavior for objects that are proofs of a statement in :g:`Prop`. This option
+      controls this behavior.
 
 .. tacn:: inversion @ident
    :name: inversion
@@ -2406,7 +2411,7 @@ Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification,
 and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new
 subgoals.
 
-.. exn:: The @term provided does not end with an equation
+.. exn:: The @term provided does not end with an equation.
 
 .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal.
 
@@ -2430,8 +2435,8 @@ subgoals.
         In particular a failure will happen if any of these three simpler tactics
         fails.
       + :n:`rewrite H in * |-` will do :n:`rewrite H in H`:sub:`i` for all hypotheses
-        :g:`H`:sub:`i` :g:`<> H`. A success will happen as soon as at least one of these
-        simpler tactics succeeds.
+        :g:`H`:sub:`i` different from :g:`H`.
+        A success will happen as soon as at least one of these simpler tactics succeeds.
       + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-`
         that succeeds if at least one of these two tactics succeeds.
 
@@ -2484,7 +2489,7 @@ subgoals.
    the assumption, or if its symmetric form occurs. It is equivalent to
    :n:`cut @term = @term; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`.
 
-.. exn:: @terms do not have convertible types
+.. exn:: @terms do not have convertible types.
 
 .. tacv:: replace @term with @term by tactic
 
@@ -2629,7 +2634,7 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
    with `U` providing that `U` is well-formed and that `T` and `U` are
    convertible.
 
-.. exn:: Not convertible
+.. exn:: Not convertible.
 
 
 .. tacv:: change @term with @term
@@ -2642,7 +2647,7 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
   This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term by @term`
   in the current goal. The terms :n:`@term` and :n:`@term` must be convertible.
 
-.. exn:: Too few occurrences
+.. exn:: Too few occurrences.
 
 .. tacv:: change @term in @ident
 .. tacv:: change @term with @term in @ident
@@ -2817,7 +2822,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    definition (say :g:`t`) and then reduces
    :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules.
 
-.. exn:: Not reducible
+.. exn:: Not reducible.
 
 .. tacn:: hnf
    :name: hnf
@@ -2944,7 +2949,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
    matching :n:`@pattern` in the current goal.
 
-   .. exn:: Too few occurrences
+   .. exn:: Too few occurrences.
 
 .. tacv:: simpl @qualid
 .. tacv:: simpl @string
@@ -2974,7 +2979,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :n:`@qualid` refers in the current goal and then replaces it with its
    :math:`\beta`:math:`\iota`-normal form.
 
-.. exn:: @qualid does not denote an evaluable constant
+.. exn:: @qualid does not denote an evaluable constant.
 
 .. tacv:: unfold @qualid in @ident
 
@@ -2991,9 +2996,9 @@ the conversion in hypotheses :n:`{+ @ident}`.
    The lists :n:`{+, @num}` specify the occurrences of :n:`@qualid` to be
    unfolded. Occurrences are located from left to right.
 
-   .. exn:: bad occurrence number of @qualid
+   .. exn:: Bad occurrence number of @qualid.
 
-   .. exn:: @qualid does not occur
+   .. exn:: @qualid does not occur.
 
 .. tacv:: unfold @string
 
@@ -3083,7 +3088,7 @@ Conversion tactics applied to hypotheses
 
    Example: :n:`unfold not in (Type of H1) (Type of H3)`.
 
-.. exn:: No such hypothesis : ident.
+.. exn:: No such hypothesis: @ident.
 
 
 .. _automation:
@@ -3134,6 +3139,7 @@ hints of the database named core.
    to know what lemmas/assumptions were used.
 
 .. tacv:: debug auto
+   :name: debug auto
 
    Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal,
    including failing paths.
@@ -3153,7 +3159,9 @@ hints of the database named core.
 .. tacv:: trivial with *
 .. tacv:: trivial using {+ @lemma}
 .. tacv:: debug trivial
+   :name: debug trivial
 .. tacv:: info_trivial
+   :name: info_trivial
 .. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}}
 
 .. note::
@@ -3263,7 +3271,8 @@ See also: :tacn:`autorewrite` for examples showing the use of this tactic.
 
    This tactic tries to solve the current goal by a number of standard closing steps.
    In particular, it tries to close the current goal using the closing tactics
-   :tacn:`trivial`, reflexivity, symmetry, contradiction and inversion of hypothesis.
+   :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction`
+   and :tacn:`inversion` of hypothesis.
    If this fails, it tries introducing variables and splitting and-hypotheses,
    using the closing tactics afterwards, and splitting the goal using
    :tacn:`split` and recursing.
@@ -3274,7 +3283,7 @@ See also: :tacn:`autorewrite` for examples showing the use of this tactic.
 .. tacv:: now @tactic
    :name: now
 
-   Run :n:`@tac` followed by ``easy``. This is a notation for :n:`@tactic; easy`.
+   Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`.
 
 Controlling automation
 --------------------------
@@ -3284,40 +3293,42 @@ Controlling automation
 The hints databases for auto and eauto
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The hints for ``auto`` and ``eauto`` are stored in databases. Each database
-maps head symbols to a list of hints. One can use the command
+The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database
+maps head symbols to a list of hints.
 
 .. cmd:: Print Hint @ident
 
-to display the hints associated to the head symbol :n:`@ident`
-(see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative
-integer, and an optional pattern. The hints with lower cost are tried first. A
-hint is tried by ``auto`` when the conclusion of the current goal matches its
-pattern or when it has no pattern.
+   Use this command
+   to display the hints associated to the head symbol :n:`@ident`
+   (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative
+   integer, and an optional pattern. The hints with lower cost are tried first. A
+   hint is tried by :tacn:`auto` when the conclusion of the current goal matches its
+   pattern or when it has no pattern.
 
 Creating Hint databases
 ```````````````````````
 
-One can optionally declare a hint database using the command ``Create
-HintDb``. If a hint is added to an unknown database, it will be
+One can optionally declare a hint database using the command
+:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be
 automatically created.
 
-.. cmd:: Create HintDb @ident {? discriminated}.
-
-This command creates a new database named :n:`@ident`. The database is
-implemented by a Discrimination Tree (DT) that serves as an index of
-all the lemmas. The DT can use transparency information to decide if a
-constant should be indexed or not (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`),
-making the retrieval more efficient. The legacy implementation (the default one
-for new databases) uses the DT only on goals without existentials (i.e., ``auto``
-goals), for non-Immediate hints and do not make use of transparency
-hints, putting more work on the unification that is run after
-retrieval (it keeps a list of the lemmas in case the DT is not used).
-The new implementation enabled by the discriminated option makes use
-of DTs in all cases and takes transparency information into account.
-However, the order in which hints are retrieved from the DT may differ
-from the order in which they were inserted, making this implementation
-observationally different from the legacy one.
+.. cmd:: Create HintDb @ident {? discriminated}
+
+   This command creates a new database named :n:`@ident`. The database is
+   implemented by a Discrimination Tree (DT) that serves as an index of
+   all the lemmas. The DT can use transparency information to decide if a
+   constant should be indexed or not
+   (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`),
+   making the retrieval more efficient. The legacy implementation (the default one
+   for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto`
+   goals), for non-Immediate hints and do not make use of transparency
+   hints, putting more work on the unification that is run after
+   retrieval (it keeps a list of the lemmas in case the DT is not used).
+   The new implementation enabled by the discriminated option makes use
+   of DTs in all cases and takes transparency information into account.
+   However, the order in which hints are retrieved from the DT may differ
+   from the order in which they were inserted, making this implementation
+   observationally different from the legacy one.
 
 The general command to add a hint to some databases :n:`{+ @ident}` is
 
@@ -3341,21 +3352,21 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
    .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}}
       :name: Hint Resolve
 
-   This command adds :n:`simple apply @term` to the hint list with the head
-   symbol of the type of :n:`@term`. The cost of that hint is the number of
-   subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The
-   associated :n:`@pattern` is inferred from the conclusion of the type of
-   :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type
-   of :n:`@term` does not start with a product the tactic added in the hint list
-   is :n:`exact @term`. In case this type can however be reduced to a type
-   starting with a product, the tactic :n:`simple apply @term` is also stored in
-   the hints list. If the inferred type of :n:`@term` contains a dependent
-   quantification on a variable which occurs only in the premisses of the type
-   and not in its conclusion, no instance could be inferred for the variable by
-   unification with the goal. In this case, the hint is added to the hint list
-   of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A
-   typical example of a hint that is used only by :tacn:`eauto` is a transitivity
-   lemma.
+      This command adds :n:`simple apply @term` to the hint list with the head
+      symbol of the type of :n:`@term`. The cost of that hint is the number of
+      subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The
+      associated :n:`@pattern` is inferred from the conclusion of the type of
+      :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type
+      of :n:`@term` does not start with a product the tactic added in the hint list
+      is :n:`exact @term`. In case this type can however be reduced to a type
+      starting with a product, the tactic :n:`simple apply @term` is also stored in
+      the hints list. If the inferred type of :n:`@term` contains a dependent
+      quantification on a variable which occurs only in the premisses of the type
+      and not in its conclusion, no instance could be inferred for the variable by
+      unification with the goal. In this case, the hint is added to the hint list
+      of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A
+      typical example of a hint that is used only by :tacn:`eauto` is a transitivity
+      lemma.
 
    .. exn:: @term cannot be used as a hint
 
@@ -3383,7 +3394,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       This command adds :n:`simple apply @term; trivial` to the hint list associated
       with the head symbol of the type of :n:`@ident` in the given database. This
       tactic will fail if all the subgoals generated by :n:`simple apply @term` are
-      not solved immediately by the ``trivial`` tactic (which only tries tactics
+      not solved immediately by the :tacn:`trivial` tactic (which only tries tactics
       with cost 0).This command is useful for theorems such as the symmetry of
       equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited
       use in order to avoid useless proof-search. The cost of this tactic (which
@@ -3421,7 +3432,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       Adds each :n:`Hint Unfold @ident`.
 
    .. cmdv:: Hint %( Transparent %| Opaque %) @qualid
-      :name: Hint ( Transparent | Opaque )
+      :name: Hint %( Transparent %| Opaque %)
 
       This adds a transparency hint to the database, making :n:`@qualid` a
       transparent or opaque constant during resolution. This information is used
@@ -3429,52 +3440,54 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       discrimination network to relax or constrain it in the case of discriminated
       databases.
 
-    .. cmdv:: Hint %(Transparent | Opaque) {+ @ident}
+   .. cmdv:: Hint %( Transparent %| Opaque %) {+ @ident}
 
       Declares each :n:`@ident` as a transparent or opaque constant.
 
-    .. cmdv:: Hint Extern @num {? @pattern} => tactic
+   .. cmdv:: Hint Extern @num {? @pattern} => tactic
+
+      This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
+      :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
+      :n:`@tactic` to execute.
 
-       This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
-       :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
-       :n:`@tactic` to execute.
+      .. example::
 
-       .. example::
+         .. coqtop:: in
 
-          .. coqtop:: in
+            Hint Extern 4 (~(_ = _)) => discriminate.
 
-             Hint Extern 4 (~(_ = _)) => discriminate.
+         Now, when the head of the goal is a disequality, ``auto`` will try
+         discriminate if it does not manage to solve the goal with hints with a
+         cost less than 4.
 
-       Now, when the head of the goal is a disequality, ``auto`` will try
-       discriminate if it does not manage to solve the goal with hints with a
-       cost less than 4. One can even use some sub-patterns of the pattern in
-       the tactic script. A sub-pattern is a question mark followed by an
-       identifier, like ``?X1`` or ``?X2``. Here is an example:
+      One can even use some sub-patterns of the pattern in
+      the tactic script. A sub-pattern is a question mark followed by an
+      identifier, like ``?X1`` or ``?X2``. Here is an example:
 
-       .. example::
+      .. example::
 
-          .. coqtop:: reset all
+         .. coqtop:: reset all
 
-             Require Import List.
-             Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
-             Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
-             Info 1 auto with eqdec.
+            Require Import List.
+            Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
+            Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
+            Info 1 auto with eqdec.
 
-    .. cmdv:: Hint Cut @regexp
+   .. cmdv:: Hint Cut @regexp
 
-       .. warning::
+      .. warning::
 
-          These hints currently only apply to typeclass proof search and the
-          :tacn:`typeclasses eauto` tactic.
+         These hints currently only apply to typeclass proof search and the
+         :tacn:`typeclasses eauto` tactic.
 
-       This command can be used to cut the proof-search tree according to a regular
-       expression matching paths to be cut. The grammar for regular expressions is
-       the following. Beware, there is no operator precedence during parsing, one can
-       check with :cmd:`Print HintDb` to verify the current cut expression:
+      This command can be used to cut the proof-search tree according to a regular
+      expression matching paths to be cut. The grammar for regular expressions is
+      the following. Beware, there is no operator precedence during parsing, one can
+      check with :cmd:`Print HintDb` to verify the current cut expression:
 
-       .. productionlist:: `regexp`
+      .. productionlist:: `regexp`
           e : ident      hint or instance identifier
-            :|_         any hint
+            :| _         any hint
             :| e\|e′     disjunction
             :| e e′      sequence
             :| e *       Kleene star
@@ -3482,42 +3495,42 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
             :| eps       epsilon
             :| ( e  )
 
-       The `emp` regexp does not match any search path while `eps`
-       matches the empty path. During proof search, the path of
-       successive successful hints on a search branch is recorded, as a
-       list of identifiers for the hints (note Hint Extern’s do not have
-       an associated identifier).
-       Before applying any hint :n:`@ident` the current path `p` extended with
-       :n:`@ident` is matched against the current cut expression `c` associated to
-       the hint database. If matching succeeds, the hint is *not* applied. The
-       semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the
-       initial cut expression being `emp`.
-
-    .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
-
-       This sets an optional mode of use of the identifier :n:`@qualid`. When
-       proof-search faces a goal that ends in an application of :n:`@qualid` to
-       arguments :n:`@term ... @term`, the mode tells if the hints associated to
-       :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``,
-       ``!`` or ``-`` items that specify if an argument of the identifier is to be
-       treated as an input (``+``), if its head only is an input (``!``) or an output
-       (``-``) of the identifier. For a mode to match a list of arguments, input
-       terms and input heads *must not* contain existential variables or be
-       existential variables respectively, while outputs can be any term. Multiple
-       modes can be declared for a single identifier, in that case only one mode
-       needs to match the arguments for the hints to be applied.The head of a term
-       is understood here as the applicative head, or the match or projection
-       scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is
-       especially useful for typeclasses, when one does not want to support default
-       instances and avoid ambiguity in general. Setting a parameter of a class as an
-       input forces proof-search to be driven by that index of the class, with ``!``
-       giving more flexibility by allowing existentials to still appear deeper in the
-       index but not at its head.
-
-    .. note::
-
-       One can use an ``Extern`` hint with no pattern to do pattern-matching on
-       hypotheses using ``match goal`` with inside the tactic.
+      The `emp` regexp does not match any search path while `eps`
+      matches the empty path. During proof search, the path of
+      successive successful hints on a search branch is recorded, as a
+      list of identifiers for the hints (note Hint Extern’s do not have
+      an associated identifier).
+      Before applying any hint :n:`@ident` the current path `p` extended with
+      :n:`@ident` is matched against the current cut expression `c` associated to
+      the hint database. If matching succeeds, the hint is *not* applied. The
+      semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the
+      initial cut expression being `emp`.
+
+   .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
+
+      This sets an optional mode of use of the identifier :n:`@qualid`. When
+      proof-search faces a goal that ends in an application of :n:`@qualid` to
+      arguments :n:`@term ... @term`, the mode tells if the hints associated to
+      :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``,
+      ``!`` or ``-`` items that specify if an argument of the identifier is to be
+      treated as an input (``+``), if its head only is an input (``!``) or an output
+      (``-``) of the identifier. For a mode to match a list of arguments, input
+      terms and input heads *must not* contain existential variables or be
+      existential variables respectively, while outputs can be any term. Multiple
+      modes can be declared for a single identifier, in that case only one mode
+      needs to match the arguments for the hints to be applied.The head of a term
+      is understood here as the applicative head, or the match or projection
+      scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is
+      especially useful for typeclasses, when one does not want to support default
+      instances and avoid ambiguity in general. Setting a parameter of a class as an
+      input forces proof-search to be driven by that index of the class, with ``!``
+      giving more flexibility by allowing existentials to still appear deeper in the
+      index but not at its head.
+
+   .. note::
+
+      One can use an ``Extern`` hint with no pattern to do pattern-matching on
+      hypotheses using ``match goal`` with inside the tactic.
 
 
 Hint databases defined in the Coq standard library
@@ -3639,7 +3652,7 @@ described above: either they disappear at the end of a section scope,
 or they remain global forever. This causes a scalability issue,
 because hints coming from an unrelated part of the code may badly
 influence another development. It can be mitigated to some extent
-thanks to the ``Remove Hints`` command (see :ref:`Remove Hints <removehints>`),
+thanks to the :cmd:`Remove Hints` command,
 but this is a mere workaround and has some limitations (for instance, external
 hints cannot be removed).
 
@@ -3647,7 +3660,7 @@ A proper way to fix this issue is to bind the hints to their module scope, as
 for most of the other objects Coq uses. Hints should only made available when
 the module they are defined in is imported, not just required. It is very
 difficult to change the historical behavior, as it would break a lot of scripts.
-We propose a smooth transitional path by providing the ``Loose Hint Behavior``
+We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior`
 option which accepts three flags allowing for a fine-grained handling of
 non-imported hints.
 
@@ -3857,7 +3870,7 @@ inductive definition.
 
   This combines the effects of the different variants of :tacn:`firstorder`.
 
-.. opt:: Firstorder Depth @natural
+.. opt:: Firstorder Depth @num
 
    This option controls the proof-search depth bound.
 
@@ -3900,11 +3913,12 @@ match against it.
   hypotheses using assert in order for :tacn:`congruence` to use them.
 
 .. tacv:: congruence with {+ @term}
+   :name: congruence with
 
-  Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps
-  in case you have partially applied constructors in your goal.
+   Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps
+   in case you have partially applied constructors in your goal.
 
-.. exn:: I don’t know how to handle dependent equality
+.. exn:: I don’t know how to handle dependent equality.
 
   The decision procedure managed to find a proof of the goal or of a
   discriminable equality but this proof could not be built in Coq because of
@@ -3916,7 +3930,7 @@ match against it.
   arguments are supplied for some partially applied constructors. Any term of an
   appropriate type will allow the tactic to successfully solve the goal. Those
   additional arguments can be given to congruence by filling in the holes in the
-  terms given in the error message, using the with variant described above.
+  terms given in the error message, using the :tacn:`congruence with` variant described above.
 
 .. opt:: Congruence Verbose
 
@@ -3935,7 +3949,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its arguments are equal modulo alpha
    conversion and casts.
 
-.. exn:: Not equal
+.. exn:: Not equal.
 
 .. tacn:: unify @term @term
    :name: unify
@@ -3943,7 +3957,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its arguments are unifiable, potentially
    instantiating existential variables.
 
-.. exn:: Not unifiable
+.. exn:: Not unifiable.
 
 .. tacv:: unify @term @term with @ident
 
@@ -3957,7 +3971,7 @@ succeeds, and results in an error otherwise.
    variable. Existential variables are uninstantiated variables generated
    by :tacn:`eapply` and some other tactics.
 
-.. exn:: Not an evar
+.. exn:: Not an evar.
 
 .. tacn:: has_evar @term
    :name: has_evar
@@ -3966,7 +3980,7 @@ succeeds, and results in an error otherwise.
    a subterm. Unlike context patterns combined with ``is_evar``, this tactic
    scans all subterms, including those under binders.
 
-.. exn:: No evars
+.. exn:: No evars.
 
 .. tacn:: is_var @term
    :name: is_var
@@ -3974,7 +3988,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its argument is a variable or hypothesis in
    the current goal context or in the opened sections.
 
-.. exn:: Not a variable or hypothesis
+.. exn:: Not a variable or hypothesis.
 
 
 .. _equality:
@@ -4001,7 +4015,7 @@ This tactic applies to a goal that has the form :g:`t=u`. It checks that `t`
 and `u` are convertible and then solves the goal. It is equivalent to apply
 :tacn:`refl_equal`.
 
-.. exn:: The conclusion is not a substitutive equation
+.. exn:: The conclusion is not a substitutive equation.
 
 .. exn:: Unable to unify ... with ...
 
@@ -4119,8 +4133,8 @@ Inversion
 available after a ``Require Import FunInd``.
 
 
-.. exn:: Hypothesis @ident must contain at least one Function
-.. exn:: Cannot find inversion information for hypothesis @ident
+.. exn:: Hypothesis @ident must contain at least one Function.
+.. exn:: Cannot find inversion information for hypothesis @ident.
 
   This error may be raised when some inversion lemma failed to be generated by
   Function.
@@ -4151,7 +4165,7 @@ function :n:`@ident`. This function must be a fixpoint on a simple recursive
 datatype: see :ref:`quote` for the full details.
 
 
-.. exn:: quote: not a simple fixpoint
+.. exn:: quote: not a simple fixpoint.
 
   Happens when quote is not able to perform inversion properly.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 692ff294a6..7ba103b222 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -14,64 +14,63 @@ Displaying
 
 .. _Print:
 
-.. cmd:: Print @qualid.
+.. cmd:: Print @qualid
+   :name: Print
 
-This command displays on the screen information about the declared or
-defined object referred by :n:`@qualid`.
+   This command displays on the screen information about the declared or
+   defined object referred by :n:`@qualid`.
 
+   Error messages:
 
-Error messages:
+   .. exn:: @qualid not a defined object.
 
+   .. exn:: Universe instance should have length @num.
 
-.. exn:: @qualid not a defined object
+   .. exn:: This object does not support universe names.
 
-.. exn:: Universe instance should have length :n:`num`.
 
-.. exn:: This object does not support universe names.
+   .. cmdv:: Print Term @qualid
+      :name: Print Term
 
+      This is a synonym of :cmd:`Print` :n:`@qualid` when :n:`@qualid`
+      denotes a global constant.
 
-Variants:
+   .. cmdv:: Print {? Term } @qualid\@@name
 
+      This locally renames the polymorphic universes of :n:`@qualid`.
+      An underscore means the raw universe is printed.
 
-.. cmdv:: Print Term @qualid.
 
-This is a synonym to ``Print`` :n:`@qualid` when :n:`@qualid`
-denotes a global constant.
-
-.. cmdv:: About @qualid.
+.. cmd:: About @qualid
    :name: About
 
-This displays various information about the object
-denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive,
-constructor, abbreviation, …), long name, type, implicit arguments and
-argument scopes. It does not print the body of definitions or proofs.
-
-.. cmdv:: Print @qualid\@@name
+   This displays various information about the object
+   denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive,
+   constructor, abbreviation, …), long name, type, implicit arguments and
+   argument scopes. It does not print the body of definitions or proofs.
 
-This locally renames the polymorphic universes of :n:`@qualid`.
-An underscore means the raw universe is printed.
-This form can be used with ``Print Term`` and ``About``.
+   .. cmdv:: About @qualid\@@name
 
-.. cmd:: Print All.
+      This locally renames the polymorphic universes of :n:`@qualid`.
+      An underscore means the raw universe is printed.
 
-This command displays information about the current state of the
-environment, including sections and modules.
 
+.. cmd:: Print All
 
-Variants:
+   This command displays information about the current state of the
+   environment, including sections and modules.
 
+   .. cmdv:: Inspect @num
+      :name: Inspect
 
-.. cmdv:: Inspect @num.
-   :name: Inspect
+      This command displays the :n:`@num` last objects of the
+      current environment, including sections and modules.
 
-This command displays the :n:`@num` last objects of the
-current environment, including sections and modules.
+   .. cmdv:: Print Section @ident
 
-.. cmdv:: Print Section @ident.
-
-The name :n:`@ident` should correspond to a currently open section,
-this command displays the objects defined since the beginning of this
-section.
+      The name :n:`@ident` should correspond to a currently open section,
+      this command displays the objects defined since the beginning of this
+      section.
 
 
 .. _flags-options-tables:
@@ -87,151 +86,136 @@ handling flags, options and tables are given below.
 
 .. TODO : flag is not a syntax entry
 
-.. cmd:: Set @flag.
-
-This command switches :n:`@flag` on. The original state of :n:`@flag` is restored
-when the current module ends.
-
-Variants:
-
-.. cmdv:: Local Set @flag.
-
-This command switches :n:`@flag` on. The original state
-of :n:`@flag` is restored when the current *section* ends.
+.. cmd:: Set @flag
 
-.. cmdv:: Global Set @flag.
+   This command switches :n:`@flag` on. The original state of :n:`@flag`
+   is restored when the current module ends.
 
-This command switches :n:`@flag` on. The original state
-of :n:`@flag` is *not* restored at the end of the module. Additionally, if
-set in a file, :n:`@flag` is switched on when the file is `Require`-d.
+   .. cmdv:: Local Set @flag
 
-.. cmdv:: Export Set @flag.
+      This command switches :n:`@flag` on. The original state
+      of :n:`@flag` is restored when the current *section* ends.
 
-   This command switches :n:`@flag` on. The original state
-   of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
-   is switched on when this module is imported.
+   .. cmdv:: Global Set @flag
 
+      This command switches :n:`@flag` on. The original state
+      of :n:`@flag` is *not* restored at the end of the module. Additionally, if
+      set in a file, :n:`@flag` is switched on when the file is `Require`-d.
 
-.. cmd:: Unset @flag.
+   .. cmdv:: Export Set @flag
 
-This command switches :n:`@flag` off. The original state of :n:`@flag` is restored
-when the current module ends.
+      This command switches :n:`@flag` on. The original state
+      of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
+      is switched on when this module is imported.
 
 
-Variants:
+.. cmd:: Unset @flag
 
-.. cmdv:: Local Unset @flag.
+   This command switches :n:`@flag` off. The original state of
+   :n:`@flag` is restored when the current module ends.
 
-This command switches :n:`@flag` off. The original
-state of :n:`@flag` is restored when the current *section* ends.
+   .. cmdv:: Local Unset @flag
 
-.. cmdv:: Global Unset @flag.
+      This command switches :n:`@flag` off. The original
+      state of :n:`@flag` is restored when the current *section* ends.
 
-This command switches :n:`@flag` off. The original
-state of :n:`@flag` is *not* restored at the end of the module. Additionally,
-if set in a file, :n:`@flag` is switched off when the file is `Require`-d.
+   .. cmdv:: Global Unset @flag
 
-.. cmdv:: Export Unset @flag.
+      This command switches :n:`@flag` off. The original
+      state of :n:`@flag` is *not* restored at the end of the module. Additionally,
+      if set in a file, :n:`@flag` is switched off when the file is `Require`-d.
 
-   This command switches :n:`@flag` off. The original state
-   of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
-   is switched off when this module is imported.
+   .. cmdv:: Export Unset @flag
 
+      This command switches :n:`@flag` off. The original state
+      of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
+      is switched off when this module is imported.
 
-.. cmd:: Test @flag.
 
-This command prints whether :n:`@flag` is on or off.
+.. cmd:: Test @flag
 
+   This command prints whether :n:`@flag` is on or off.
 
-.. cmd:: Set @option @value.
 
-This command sets :n:`@option` to :n:`@value`. The original value of ` option` is
-restored when the current module ends.
+.. cmd:: Set @option @value
 
+   This command sets :n:`@option` to :n:`@value`. The original value of ` option` is
+   restored when the current module ends.
 
-Variants:
+   .. TODO : option and value are not syntax entries
 
-.. TODO : option and value are not syntax entries
+   .. cmdv:: Local Set @option @value
 
-.. cmdv:: Local Set @option @value.
+      This command sets :n:`@option` to :n:`@value`. The
+      original value of :n:`@option` is restored at the end of the module.
 
-This command sets :n:`@option` to :n:`@value`. The
-original value of :n:`@option` is restored at the end of the module.
+   .. cmdv:: Global Set @option @value
 
-.. cmdv:: Global Set @option @value.
+      This command sets :n:`@option` to :n:`@value`. The
+      original value of :n:`@option` is *not* restored at the end of the module.
+      Additionally, if set in a file, :n:`@option` is set to value when the file
+      is `Require`-d.
 
-This command sets :n:`@option` to :n:`@value`. The
-original value of :n:`@option` is *not* restored at the end of the module.
-Additionally, if set in a file, :n:`@option` is set to value when the file
-is `Require`-d.
+   .. cmdv:: Export Set @option
 
-.. cmdv:: Export Set @option.
+      This command set :n:`@option` to :n:`@value`. The original state
+      of :n:`@option` is restored at the end of the current module, but :n:`@option`
+      is set to :n:`@value` when this module is imported.
 
-   This command set :n:`@option` to :n:`@value`. The original state
-   of :n:`@option` is restored at the end of the current module, but :n:`@option`
-   is set to :n:`@value` when this module is imported.
 
-
-.. cmd::  Unset @option.
+.. cmd:: Unset @option
 
    This command turns off :n:`@option`.
 
+   .. cmdv:: Local Unset @option
 
-Variants:
-
+      This command turns off :n:`@option`. The original state of :n:`@option`
+      is restored when the current *section* ends.
 
-.. cmdv:: Local Unset @option.
+   .. cmdv:: Global Unset @option
 
-   This command turns off :n:`@option`. The original state of :n:`@option` is restored when the current
-   *section* ends.
+      This command turns off :n:`@option`. The original state of :n:`@option`
+      is *not* restored at the end of the module. Additionally, if unset in a file,
+      :n:`@option` is reset to its default value when the file is `Require`-d.
 
-.. cmdv:: Global Unset @option.
+   .. cmdv:: Export Unset @option
 
-   This command turns off :n:`@option`. The original state of :n:`@option` is *not* restored at the end of the
-   module. Additionally, if unset in a file, :n:`@option` is reset to its
-   default value when the file is `Require`-d.
+      This command turns off :n:`@option`. The original state of :n:`@option`
+      is restored at the end of the current module, but :n:`@option` is set to
+      its default value when this module is imported.
 
-.. cmdv:: Export Unset @option.
-
-   This command turns off :n:`@option`. The original state of :n:`@option` is restored at the end of the
-   current module, but :n:`@option` is set to its default value when this module
-   is imported.
 
+.. cmd:: Test @option
 
-.. cmd:: Test @option.
-
-This command prints the current value of :n:`@option`.
+   This command prints the current value of :n:`@option`.
 
 
 .. TODO : table is not a syntax entry
 
-.. cmd:: Add @table @value.
+.. cmd:: Add @table @value
    :name: Add `table` `value`
 
-.. cmd:: Remove @table @value.
+.. cmd:: Remove @table @value
    :name: Remove `table` `value`
 
-.. cmd:: Test @table @value.
+.. cmd:: Test @table @value
    :name: Test `table` `value`
 
-.. cmd:: Test @table for @value.
+.. cmd:: Test @table for @value
    :name: Test `table` for `value`
 
-.. cmd:: Print Table @table.
-
-These are  general commands for tables.
-
-.. cmd:: Print Options.
+.. cmd:: Print Table @table
 
-This command lists all available flags, options and tables.
+These are general commands for tables.
 
 
-Variants:
+.. cmd:: Print Options
 
+   This command lists all available flags, options and tables.
 
-.. cmdv:: Print Tables.
+   .. cmdv:: Print Tables
 
-This is a synonymous of ``Print Options``.
+      This is a synonymous of :cmd:`Print Options`.
 
 
 .. _requests-to-the-environment:
@@ -239,358 +223,330 @@ This is a synonymous of ``Print Options``.
 Requests to the environment
 -------------------------------
 
-.. cmd:: Check @term.
+.. cmd:: Check @term
 
-This command displays the type of :n:`@term`. When called in proof mode, the
-term is checked in the local context of the current subgoal.
+   This command displays the type of :n:`@term`. When called in proof mode, the
+   term is checked in the local context of the current subgoal.
 
 
-Variants:
+   .. TODO : selector is not a syntax entry
 
-.. TODO : selector is not a syntax entry
+   .. cmdv:: @selector: Check @term
 
-.. cmdv:: @selector: Check @term.
+      This variant specifies on which subgoal to perform typing
+      (see Section :ref:`invocation-of-tactics`).
 
-specifies on which subgoal to perform typing
-(see Section :ref:`invocation-of-tactics`).
 
 .. TODO : convtactic is not a syntax entry
 
-.. cmd:: Eval @convtactic in @term.
-
-This command performs the specified reduction on :n:`@term`, and displays
-the resulting term with its type. The term to be reduced may depend on
-hypothesis introduced in the first subgoal (if a proof is in
-progress).
-
-
-See also: Section :ref:`performingcomputations`.
-
-
-.. cmd:: Compute @term.
-
-This command performs a call-by-value evaluation of term by using the
-bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in``
-:n:`@term`.
-
-
-See also: Section :ref:`performingcomputations`.
-
-
-.. cmd::Extraction @term.
-
-This command displays the extracted term from :n:`@term`. The extraction is
-processed according to the distinction between :g:`Set` and :g:`Prop`; that is
-to say, between logical and computational content (see Section :ref:`sorts`).
-The extracted term is displayed in OCaml syntax, where global identifiers are
-still displayed as in |Coq| terms.
-
-
-Variants:
+.. cmd:: Eval @convtactic in @term
 
+   This command performs the specified reduction on :n:`@term`, and displays
+   the resulting term with its type. The term to be reduced may depend on
+   hypothesis introduced in the first subgoal (if a proof is in
+   progress).
 
-.. cmdv:: Recursive Extraction {+ @qualid }.
+   See also: Section :ref:`performingcomputations`.
 
-Recursively extracts all
-the material needed for the extraction of the qualified identifiers.
 
+.. cmd:: Compute @term
 
-See also: Chapter :ref:`extraction`.
+   This command performs a call-by-value evaluation of term by using the
+   bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in``
+   :n:`@term`.
 
+   See also: Section :ref:`performingcomputations`.
 
-.. cmd:: Print Assumptions @qualid.
 
-This commands display all the assumptions (axioms, parameters and
-variables) a theorem or definition depends on. Especially, it informs
-on the assumptions with respect to which the validity of a theorem
-relies.
+.. cmd:: Print Assumptions @qualid
 
+   This commands display all the assumptions (axioms, parameters and
+   variables) a theorem or definition depends on. Especially, it informs
+   on the assumptions with respect to which the validity of a theorem
+   relies.
 
-Variants:
+   .. cmdv:: Print Opaque Dependencies @qualid
+      :name: Print Opaque Dependencies
 
+      Displays the set of opaque constants :n:`@qualid` relies on in addition to
+      the assumptions.
 
-.. cmdv:: Print Opaque Dependencies @qualid.
+   .. cmdv:: Print Transparent Dependencies @qualid
+      :name: Print Transparent Dependencies
 
-Displays the set of opaque constants :n:`@qualid` relies on in addition to
-the assumptions.
+      Displays the set of transparent constants :n:`@qualid` relies on
+      in addition to the assumptions.
 
-.. cmdv:: Print Transparent Dependencies @qualid.
+   .. cmdv:: Print All Dependencies @qualid
+      :name: Print All Dependencies
 
-Displays the set of
-transparent constants :n:`@qualid` relies on in addition to the assumptions.
+      Displays all assumptions and constants :n:`@qualid` relies on.
 
-.. cmdv:: Print All Dependencies @qualid.
 
-Displays all assumptions and constants :n:`@qualid` relies on.
+.. cmd:: Search @qualid
 
+   This command displays the name and type of all objects (hypothesis of
+   the current goal, theorems, axioms, etc) of the current context whose
+   statement contains :n:`@qualid`. This command is useful to remind the user
+   of the name of library lemmas.
 
+   .. exn:: The reference @qualid was not found in the current environment.
 
-.. cmd:: Search @qualid.
+      There is no constant in the environment named qualid.
 
-This command displays the name and type of all objects (hypothesis of
-the current goal, theorems, axioms, etc) of the current context whose
-statement contains :n:`@qualid`. This command is useful to remind the user
-of the name of library lemmas.
+   .. cmdv:: Search @string
 
+      If :n:`@string` is a valid identifier, this command
+      displays the name and type of all objects (theorems, axioms, etc) of
+      the current context whose name contains string. If string is a
+      notation’s string denoting some reference :n:`@qualid` (referred to by its
+      main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or
+      `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`.
 
-Error messages:
+   .. cmdv:: Search @string%@key
 
+      The string string must be a notation or the main
+      symbol of a notation which is then interpreted in the scope bound to
+      the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`).
 
-.. exn:: The reference @qualid was not found in the current environment
+   .. cmdv:: Search @term_pattern
 
-There is no constant in the environment named qualid.
+      This searches for all statements or types of
+      definition that contains a subterm that matches the pattern
+      `term_pattern` (holes of the pattern are either denoted by `_` or by
+      `?ident` when non linear patterns are expected).
 
-Variants:
+   .. cmdv:: Search { + [-]@term_pattern_string }
 
-.. cmdv:: Search @string.
+      where
+      :n:`@term_pattern_string` is a term_pattern, a string, or a string followed
+      by a scope delimiting key `%key`.  This generalization of ``Search`` searches
+      for all objects whose statement or type contains a subterm matching
+      :n:`@term_pattern` (or :n:`@qualid` if :n:`@string` is the notation for a reference
+      qualid) and whose name contains all string of the request that
+      correspond to valid identifiers. If a term_pattern or a string is
+      prefixed by `-`, the search excludes the objects that mention that
+      term_pattern or that string.
 
-If :n:`@string` is a valid identifier, this command
-displays the name and type of all objects (theorems, axioms, etc) of
-the current context whose name contains string. If string is a
-notation’s string denoting some reference :n:`@qualid` (referred to by its
-main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or
-`"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`.
+   .. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid }
 
-.. cmdv:: Search @string%@key.
+      This restricts the search to constructions defined in the modules
+      named by the given :n:`qualid` sequence.
 
-The string string must be a notation or the main
-symbol of a notation which is then interpreted in the scope bound to
-the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`).
+   .. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }
 
-.. cmdv:: Search @term_pattern.
+      This restricts the search to constructions not defined in the modules
+      named by the given :n:`qualid` sequence.
 
-This searches for all statements or types of
-definition that contains a subterm that matches the pattern
-`term_pattern` (holes of the pattern are either denoted by `_` or by
-`?ident` when non linear patterns are expected).
+   .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string
 
-.. cmdv:: Search { + [-]@term_pattern_string }.
+      This specifies the goal on which to search hypothesis (see
+      Section :ref:`invocation-of-tactics`).
+      By default the 1st goal is searched. This variant can
+      be combined with other variants presented here.
 
-where
-:n:`@term_pattern_string` is a term_pattern, a string, or a string followed
-by a scope delimiting key `%key`.  This generalization of ``Search`` searches
-for all objects whose statement or type contains a subterm matching
-:n:`@term_pattern` (or :n:`@qualid` if :n:`@string` is the notation for a reference
-qualid) and whose name contains all string of the request that
-correspond to valid identifiers. If a term_pattern or a string is
-prefixed by `-`, the search excludes the objects that mention that
-term_pattern or that string.
+      .. example::
 
-.. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid } .
+         .. coqtop:: in
 
-This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
+            Require Import ZArith.
 
-.. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }.
+         .. coqtop:: all
 
-This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
+            Search Z.mul Z.add "distr".
 
-.. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string.
+            Search "+"%Z "*"%Z "distr" -positive -Prop.
 
-This specifies the goal on which to search hypothesis (see
-Section :ref:`invocation-of-tactics`).
-By default the 1st goal is searched. This variant can
-be combined with other variants presented here.
+            Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 
+   .. cmdv:: SearchAbout
 
-.. coqtop:: in
+      .. deprecated:: 8.5
 
-   Require Import ZArith.
+      Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current
+      :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with
+      command :cmd:`SearchAbout`. For compatibility, the deprecated name
+      :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For
+      compatibility, the list of objects to search when using :cmd:`SearchAbout`
+      may also be enclosed by optional ``[ ]`` delimiters.
 
-.. coqtop:: all
 
-   Search Z.mul Z.add "distr".
+.. cmd:: SearchHead @term
 
-   Search "+"%Z "*"%Z "distr" -positive -Prop.
+   This command displays the name and type of all hypothesis of the
+   current goal (if any) and theorems of the current context whose
+   statement’s conclusion has the form `(term t1 .. tn)`. This command is
+   useful to remind the user of the name of library lemmas.
 
-   Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
+   .. example::
 
-.. note:: Up to |Coq| version 8.4, ``Search`` had the behavior of current
-   ``SearchHead`` and the behavior of current Search was obtained with
-   command ``SearchAbout``. For compatibility, the deprecated name
-   SearchAbout can still be used as a synonym of Search. For
-   compatibility, the list of objects to search when using ``SearchAbout``
-   may also be enclosed by optional ``[ ]`` delimiters.
+      .. coqtop:: reset all
 
+         SearchHead le.
 
-.. cmd:: SearchHead @term.
+         SearchHead (@eq bool).
 
-This command displays the name and type of all hypothesis of the
-current goal (if any) and theorems of the current context whose
-statement’s conclusion has the form `(term t1 .. tn)`. This command is
-useful to remind the user of the name of library lemmas.
+   .. cmdv:: SearchHead @term inside {+ @qualid }
 
+      This restricts the search to constructions defined in the modules named
+      by the given :n:`qualid` sequence.
 
+   .. cmdv:: SearchHead term outside {+ @qualid }
 
-.. coqtop:: reset all
+      This restricts the search to constructions not defined in the modules
+      named by the given :n:`qualid` sequence.
 
-   SearchHead le.
+   .. exn:: Module/section @qualid not found.
 
-   SearchHead (@eq bool).
+      No module :n:`@qualid` has been required (see Section :ref:`compiled-files`).
 
+   .. cmdv:: @selector: SearchHead @term
 
-Variants:
+      This specifies the goal on which to
+      search hypothesis (see Section :ref:`invocation-of-tactics`).
+      By default the 1st goal is searched. This variant can be combined
+      with other variants presented here.
 
-.. cmdv:: SearchHead @term inside {+ @qualid }.
+   .. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``.
 
-This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: SearchHead term outside {+ @qualid }.
+.. cmd:: SearchPattern @term
 
-This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
+   This command displays the name and type of all hypothesis of the
+   current goal (if any) and theorems of the current context whose
+   statement’s conclusion or last hypothesis and conclusion matches the
+   expressionterm where holes in the latter are denoted by `_`.
+   It is a variant of Search @term_pattern that does not look for subterms
+   but searches for statements whose conclusion has exactly the expected
+   form, or whose statement finishes by the given series of
+   hypothesis/conclusion.
 
-Error messages:
+   .. example::
 
-.. exn:: Module/section @qualid not found
+      .. coqtop:: in
 
-No module :n:`@qualid` has been required
-(see Section :ref:`compiled-files`).
+         Require Import Arith.
 
-.. cmdv:: @selector: SearchHead @term.
+      .. coqtop:: all
 
-This specifies the goal on which to
-search hypothesis (see Section :ref:`invocation-of-tactics`).
-By default the 1st goal is
-searched. This variant can be combined with other variants presented
-here.
+         SearchPattern (_ + _ = _ + _).
 
-.. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``.
+         SearchPattern (nat -> bool).
 
+         SearchPattern (forall l : list _, _ l l).
 
-.. cmd:: SearchPattern @term.
+   Patterns need not be linear: you can express that the same expression
+   must occur in two places by using pattern variables `?ident`.
 
-This command displays the name and type of all hypothesis of the
-current goal (if any) and theorems of the current context whose
-statement’s conclusion or last hypothesis and conclusion matches the
-expressionterm where holes in the latter are denoted by `_`.
-It is a
-variant of Search @term_pattern that does not look for subterms but
-searches for statements whose conclusion has exactly the expected
-form, or whose statement finishes by the given series of
-hypothesis/conclusion.
 
-.. coqtop:: in
+   .. example::
 
-   Require Import Arith.
+      .. coqtop:: all
 
-.. coqtop:: all
+         SearchPattern (?X1 + _ = _ + ?X1).
 
-    SearchPattern (_ + _ = _ + _).
+   .. cmdv:: SearchPattern @term inside {+ @qualid }
 
-    SearchPattern (nat -> bool).
+      This restricts the search to constructions defined in the modules
+      named by the given :n:`qualid` sequence.
 
-    SearchPattern (forall l : list _, _ l l).
+   .. cmdv:: SearchPattern @term outside {+ @qualid }
 
-Patterns need not be linear: you can express that the same expression
-must occur in two places by using pattern variables `?ident`.
+      This restricts the search to constructions not defined in the modules
+      named by the given :n:`qualid` sequence.
 
+   .. cmdv:: @selector: SearchPattern @term
 
-.. coqtop:: all
+      This specifies the goal on which to
+      search hypothesis (see Section :ref:`invocation-of-tactics`).
+      By default the 1st goal is
+      searched. This variant can be combined with other variants presented
+      here.
 
-   SearchPattern (?X1 + _ = _ + ?X1).
 
-Variants:
+.. cmd:: SearchRewrite @term
 
+   This command displays the name and type of all hypothesis of the
+   current goal (if any) and theorems of the current context whose
+   statement’s conclusion is an equality of which one side matches the
+   expression term. Holes in term are denoted by “_”.
 
-.. cmdv:: SearchPattern @term inside {+ @qualid } .
+   .. example::
 
-This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
+      .. coqtop:: in
 
-.. cmdv:: SearchPattern @term outside {+ @qualid }.
+         Require Import Arith.
 
-This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
+      .. coqtop:: all
 
-.. cmdv:: @selector: SearchPattern @term.
+         SearchRewrite (_ + _ + _).
 
-This specifies the goal on which to
-search hypothesis (see Section :ref:`invocation-of-tactics`). By default the 1st goal is
-searched. This variant can be combined with other variants presented
-here.
+   .. cmdv:: SearchRewrite term inside {+ @qualid }
 
+      This restricts the search to constructions defined in the modules
+      named by the given :n:`qualid` sequence.
 
+   .. cmdv:: SearchRewrite @term outside {+ @qualid }
 
-.. cmdv:: SearchRewrite @term.
+      This restricts the search to constructions not defined in the modules
+      named by the given :n:`qualid` sequence.
 
-This command displays the name and type of all hypothesis of the
-current goal (if any) and theorems of the current context whose
-statement’s conclusion is an equality of which one side matches the
-expression term. Holes in term are denoted by “_”.
+   .. cmdv:: @selector: SearchRewrite @term
 
-.. coqtop:: in
-
-    Require Import Arith.
-
-.. coqtop:: all
-
-    SearchRewrite (_ + _ + _).
-
-Variants:
-
-
-.. cmdv:: SearchRewrite term inside {+ @qualid }.
-
-This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
-
-.. cmdv:: SearchRewrite @term outside {+ @qualid }.
-
-This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
-
-.. cmdv:: @selector: SearchRewrite @term.
-
-This specifies the goal on which to
-search hypothesis (see Section :ref:`invocation-of-tactics`). By default the 1st goal is
-searched. This variant can be combined with other variants presented
-here.
+      This specifies the goal on which to
+      search hypothesis (see Section :ref:`invocation-of-tactics`).
+      By default the 1st goal is
+      searched. This variant can be combined with other variants presented
+      here.
 
 .. note::
 
-   For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite``
-   queries, it
-   is possible to globally filter the search results via the command
-   ``Add Search Blacklist`` :n:`@substring`. A lemma whose fully-qualified name
-   contains any of the declared substrings will be removed from the
-   search results. The default blacklisted substrings are ``_subproof``
-   ``Private_``. The command ``Remove Search Blacklist ...`` allows expunging
-   this blacklist.
-
+   .. cmd:: Add Search Blacklist @string
 
-.. cmd:: Locate @qualid.
+      For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite``
+      queries, it is possible to globally filter the search results using this
+      command. A lemma whose fully-qualified name
+      contains any of the declared strings will be removed from the
+      search results. The default blacklisted substrings are ``_subproof`` and
+      ``Private_``.
 
-This command displays the full name of objects whose name is a prefix
-of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in
-which they are defined. It searches for objects from the different
-qualified name spaces of |Coq|: terms, modules, Ltac, etc.
+   .. cmd:: Remove Search Blacklist @string
 
-.. coqtop:: none
+      This command allows expunging this blacklist.
 
-    Set Printing Depth 50.
 
-.. coqtop:: all
+.. cmd:: Locate @qualid
 
-    Locate nat.
+   This command displays the full name of objects whose name is a prefix
+   of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in
+   which they are defined. It searches for objects from the different
+   qualified name spaces of |Coq|: terms, modules, Ltac, etc.
 
-    Locate Datatypes.O.
+   .. example::
 
-    Locate Init.Datatypes.O.
+      .. coqtop:: all
 
-    Locate Coq.Init.Datatypes.O.
+         Locate nat.
 
-    Locate I.Dont.Exist.
+         Locate Datatypes.O.
 
-Variants:
+         Locate Init.Datatypes.O.
 
+         Locate Coq.Init.Datatypes.O.
 
-.. cmdv:: Locate Term @qualid.
+         Locate I.Dont.Exist.
 
-As Locate but restricted to terms.
+   .. cmdv:: Locate Term @qualid
 
-.. cmdv:: Locate Module @qualid.
+      As Locate but restricted to terms.
 
-As Locate but restricted to modules.
+   .. cmdv:: Locate Module @qualid
 
-.. cmdv:: Locate Ltac @qualid.
+      As Locate but restricted to modules.
 
-As Locate but restricted to tactics.
+   .. cmdv:: Locate Ltac @qualid
 
+      As Locate but restricted to tactics.
 
 See also: Section :ref:`locating-notations`
 
@@ -608,40 +564,35 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
 (and default) extension of |Coq|’s script files is .v.
 
 
-.. cmd:: Load @ident.
-
-This command loads the file named :n:`ident`.v, searching successively in
-each of the directories specified in the *loadpath*. (see Section
-:ref:`libraries-and-filesystem`)
+.. cmd:: Load @ident
 
-Files loaded this way cannot leave proofs open, and the ``Load``
-command cannot be used inside a proof either.
+   This command loads the file named :n:`ident`.v, searching successively in
+   each of the directories specified in the *loadpath*. (see Section
+   :ref:`libraries-and-filesystem`)
 
-Variants:
+   Files loaded this way cannot leave proofs open, and the ``Load``
+   command cannot be used inside a proof either.
 
+   .. cmdv:: Load @string
 
-.. cmdv:: Load @string.
+      Loads the file denoted by the string :n:`@string`, where
+      string is any complete filename. Then the `~` and .. abbreviations are
+      allowed as well as shell variables. If no extension is specified, |Coq|
+      will use the default extension ``.v``.
 
-Loads the file denoted by the string :n:`@string`, where
-string is any complete filename. Then the `~` and .. abbreviations are
-allowed as well as shell variables. If no extension is specified, |Coq|
-will use the default extension ``.v``.
+   .. cmdv:: Load Verbose @ident
 
-.. cmdv:: Load Verbose @ident.
+   .. cmdv:: Load Verbose @string
 
-.. cmdv:: Load Verbose @string.
+      Display, while loading,
+      the answers of |Coq| to each command (including tactics) contained in
+      the loaded file See also: Section :ref:`controlling-display`.
 
-Display, while loading,
-the answers of |Coq| to each command (including tactics) contained in
-the loaded file See also: Section :ref:`controlling-display`.
+   .. exn:: Can’t find file @ident on loadpath.
 
-Error messages:
+   .. exn:: Load is not supported inside proofs.
 
-.. exn:: Can’t find file @ident on loadpath
-
-.. exn:: Load is not supported inside proofs
-
-.. exn:: Files processed by Load cannot leave open proofs
+   .. exn:: Files processed by Load cannot leave open proofs.
 
 .. _compiled-files:
 
@@ -653,151 +604,137 @@ Chapter :ref:`thecoqcommands` for documentation on how to compile a file). A com
 file is a particular case of module called *library file*.
 
 
-.. cmd:: Require @qualid.
-
-This command looks in the loadpath for a file containing module :n:`@qualid`
-and adds the corresponding module to the environment of |Coq|. As
-library files have dependencies in other library files, the command
-``Require`` :n:`@qualid` recursively requires all library files the module
-qualid depends on and adds the corresponding modules to the
-environment of |Coq| too. |Coq| assumes that the compiled files have been
-produced by a valid |Coq| compiler and their contents are then not
-replayed nor rechecked.
-
-To locate the file in the file system, :n:`@qualid` is decomposed under the
-form `dirpath.ident` and the file `ident.vo` is searched in the physical
-directory of the file system that is mapped in |Coq| loadpath to the
-logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between
-physical directories and logical names at the time of requiring the
-file must be consistent with the mapping used to compile the file. If
-several files match, one of them is picked in an unspecified fashion.
+.. cmd:: Require @qualid
 
+   This command looks in the loadpath for a file containing module :n:`@qualid`
+   and adds the corresponding module to the environment of |Coq|. As
+   library files have dependencies in other library files, the command
+   :cmd:`Require` :n:`@qualid` recursively requires all library files the module
+   qualid depends on and adds the corresponding modules to the
+   environment of |Coq| too. |Coq| assumes that the compiled files have been
+   produced by a valid |Coq| compiler and their contents are then not
+   replayed nor rechecked.
 
-Variants:
+   To locate the file in the file system, :n:`@qualid` is decomposed under the
+   form `dirpath.ident` and the file `ident.vo` is searched in the physical
+   directory of the file system that is mapped in |Coq| loadpath to the
+   logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between
+   physical directories and logical names at the time of requiring the
+   file must be consistent with the mapping used to compile the file. If
+   several files match, one of them is picked in an unspecified fashion.
 
-.. cmdv:: Require Import @qualid.
 
-This loads and declares the module :n:`@qualid`
-and its dependencies then imports the contents of :n:`@qualid` as described
-:ref:`here <import_qualid>`. It does not import the modules on which
-qualid depends unless these modules were themselves required in module
-:n:`@qualid`
-using ``Require Export``, as described below, or recursively required
-through a sequence of ``Require Export``.  If the module required has
-already been loaded, ``Require Import`` :n:`@qualid` simply imports it, as ``Import``
-:n:`@qualid` would.
+   .. cmdv:: Require Import @qualid
 
-.. cmdv:: Require Export @qualid.
+      This loads and declares the module :n:`@qualid`
+      and its dependencies then imports the contents of :n:`@qualid` as described
+      :ref:`here <import_qualid>`. It does not import the modules on which
+      qualid depends unless these modules were themselves required in module
+      :n:`@qualid`
+      using :cmd:`Require Export`, as described below, or recursively required
+      through a sequence of :cmd:`Require Export`.  If the module required has
+      already been loaded, :cmd:`Require Import` :n:`@qualid` simply imports it, as
+      :cmd:`Import` :n:`@qualid` would.
 
-This command acts as ``Require Import`` :n:`@qualid`,
-but if a further module, say `A`, contains a command ``Require Export`` `B`,
-then the command ``Require Import`` `A` also imports the module `B.`
+   .. cmdv:: Require Export @qualid
 
-.. cmdv:: Require [Import | Export] {+ @qualid }.
+      This command acts as ``Require Import`` :n:`@qualid`,
+      but if a further module, say `A`, contains a command ``Require Export`` `B`,
+      then the command ``Require Import`` `A` also imports the module `B.`
 
-This loads the
-modules named by the :n:`qualid` sequence and their recursive
-dependencies. If
-``Import`` or ``Export`` is given, it also imports these modules and
-all the recursive dependencies that were marked or transitively marked
-as ``Export``.
+   .. cmdv:: Require [Import | Export] {+ @qualid }
 
-.. cmdv:: From @dirpath Require @qualid.
+      This loads the
+      modules named by the :n:`qualid` sequence and their recursive
+      dependencies. If
+      ``Import`` or ``Export`` is given, it also imports these modules and
+      all the recursive dependencies that were marked or transitively marked
+      as ``Export``.
 
-This command acts as ``Require``, but picks
-any library whose absolute name is of the form dirpath.dirpath’.qualid
-for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library
-comes from a given package by making explicit its absolute root.
+   .. cmdv:: From @dirpath Require @qualid
 
+      This command acts as ``Require``, but picks
+      any library whose absolute name is of the form dirpath.dirpath’.qualid
+      for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library
+      comes from a given package by making explicit its absolute root.
 
+   .. exn:: Cannot load qualid: no physical path bound to dirpath.
 
-Error messages:
+   .. exn:: Cannot find library foo in loadpath.
 
-.. exn:: Cannot load qualid: no physical path bound to dirpath
+      The command did not find the
+      file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a
+      directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`).
 
-.. exn:: Cannot find library foo in loadpath
+   .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid.
 
-The command did not find the
-file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a
-directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`).
+      The command tried to load library file :n:`@ident`.vo that
+      depends on some specific version of library :n:`@qualid` which is not the
+      one already loaded in the current |Coq| session. Probably `ident.v` was
+      not properly recompiled with the last version of the file containing
+      module :n:`@qualid`.
 
-.. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid
+   .. exn:: Bad magic number.
 
-The command tried to load library file :n:`@ident`.vo that
-depends on some specific version of library :n:`@qualid` which is not the
-one already loaded in the current |Coq| session. Probably `ident.v` was
-not properly recompiled with the last version of the file containing
-module :n:`@qualid`.
+      The file `ident.vo` was found but either it is not a
+      |Coq| compiled module, or it was compiled with an incompatible
+      version of |Coq|.
 
-.. exn:: Bad magic number
+   .. exn:: The file `ident.vo` contains library dirpath and not library dirpath’.
 
-The file `ident.vo` was found but either it is not a
-|Coq| compiled module, or it was compiled with an incompatible
-version of |Coq|.
+      The library file `dirpath’` is indirectly required by the
+      ``Require`` command but it is bound in the current loadpath to the
+      file `ident.vo` which was bound to a different library name `dirpath` at
+      the time it was compiled.
 
-.. exn:: The file `ident.vo` contains library dirpath and not library dirpath’
 
-The library file `dirpath’` is indirectly required by the
-``Require`` command but it is bound in the current loadpath to the
-file `ident.vo` which was bound to a different library name `dirpath` at
-the time it was compiled.
+   .. exn:: Require is not allowed inside a module or a module type.
 
-
-.. exn:: Require is not allowed inside a module or a module type
-
-This command
-is not allowed inside a module or a module type being defined. It is
-meant to describe a dependency between compilation units. Note however
-that the commands ``Import`` and ``Export`` alone can be used inside modules
-(see Section :ref:`Import <import_qualid>`).
+      This command
+      is not allowed inside a module or a module type being defined. It is
+      meant to describe a dependency between compilation units. Note however
+      that the commands ``Import`` and ``Export`` alone can be used inside modules
+      (see Section :ref:`Import <import_qualid>`).
 
 
 
 See also: Chapter :ref:`thecoqcommands`
 
 
-.. cmd:: Print Libraries.
-
-This command displays the list of library files loaded in the
-current |Coq| session. For each of these libraries, it also tells if it
-is imported.
-
-
-.. cmd:: Declare ML Module {+ @string } .
-
-This commands loads the OCaml compiled files
-with names given by the :n:`@string` sequence
-(dynamic link). It is mainly used to load tactics dynamically. The
-files are searched into the current OCaml loadpath (see the
-command ``Add ML Path`` in Section :ref:`libraries-and-filesystem`). Loading of OCaml files is only possible under the bytecode version of ``coqtop`` (i.e.
-``coqtop`` called with option ``-byte``, see chapter :ref:`thecoqcommands`), or when |Coq| has been compiled with a
-version of OCaml that supports native Dynlink (≥ 3.11).
-
-
-Variants:
-
+.. cmd:: Print Libraries
 
-.. cmdv:: Local Declare ML Module {+ @string }.
+   This command displays the list of library files loaded in the
+   current |Coq| session. For each of these libraries, it also tells if it
+   is imported.
 
-This variant is not
-exported to the modules that import the module where they occur, even
-if outside a section.
 
+.. cmd:: Declare ML Module {+ @string }
 
+   This commands loads the OCaml compiled files
+   with names given by the :n:`@string` sequence
+   (dynamic link). It is mainly used to load tactics dynamically. The
+   files are searched into the current OCaml loadpath (see the
+   command ``Add ML Path`` in Section :ref:`libraries-and-filesystem`).
+   Loading of OCaml files is only possible under the bytecode version of
+   ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter
+   :ref:`thecoqcommands`), or when |Coq| has been compiled with a
+   version of OCaml that supports native Dynlink (≥ 3.11).
 
-Error messages:
+   .. cmdv:: Local Declare ML Module {+ @string }
 
-.. exn:: File not found on loadpath : @string
+      This variant is not exported to the modules that import the module
+      where they occur, even if outside a section.
 
-.. exn:: Loading of ML object file forbidden in a native Coq
+   .. exn:: File not found on loadpath: @string.
 
+   .. exn:: Loading of ML object file forbidden in a native Coq.
 
 
-.. cmd:: Print ML Modules.
+.. cmd:: Print ML Modules
 
-This prints the name of all OCaml modules loaded with ``Declare
-ML Module``. To know from where these module were loaded, the user
-should use the command ``Locate File`` (see :ref:`here <locate-file>`)
+   This prints the name of all OCaml modules loaded with ``Declare
+   ML Module``. To know from where these module were loaded, the user
+   should use the command ``Locate File`` (see :ref:`here <locate-file>`)
 
 
 .. _loadpath:
@@ -811,110 +748,92 @@ for practical purposes. Such commands are only meant to be issued in
 the toplevel, and using them in source files is discouraged.
 
 
-.. cmd:: Pwd.
-
-This command displays the current working directory.
-
-
-.. cmd:: Cd @string.
-
-This command changes the current directory according to :n:`@string` which
-can be any valid path.
-
-
-Variants:
-
-
-.. cmdv:: Cd.
-
-Is equivalent to Pwd.
-
-
-
-.. cmd:: Add LoadPath @string as @dirpath.
-
-This command is equivalent to the command line option
-``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current
-|Coq| loadpath and maps it to the logical directory dirpath.
+.. cmd:: Pwd
 
-Variants:
+   This command displays the current working directory.
 
 
-.. cmdv:: Add LoadPath @string.
+.. cmd:: Cd @string
 
-Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but
-for the empty directory path.
+   This command changes the current directory according to :n:`@string` which
+   can be any valid path.
 
+   .. cmdv:: Cd
 
+      Is equivalent to Pwd.
 
-.. cmd:: Add Rec LoadPath @string as @dirpath.
 
-This command is equivalent to the command line option
-``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its
-subdirectories to the current |Coq| loadpath.
+.. cmd:: Add LoadPath @string as @dirpath
 
-Variants:
+   This command is equivalent to the command line option
+   ``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current
+   |Coq| loadpath and maps it to the logical directory dirpath.
 
+   .. cmdv:: Add LoadPath @string
 
-.. cmdv:: Add Rec LoadPath @string.
+      Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but
+      for the empty directory path.
 
-Works as ``Add Rec LoadPath`` :n:`@string` as :n:`@dirpath` but for the empty
-logical directory path.
 
+.. cmd:: Add Rec LoadPath @string as @dirpath
 
+   This command is equivalent to the command line option
+   ``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its
+   subdirectories to the current |Coq| loadpath.
 
-.. cmd:: Remove LoadPath @string.
+   .. cmdv:: Add Rec LoadPath @string
 
-This command removes the path :n:`@string` from the current |Coq| loadpath.
+      Works as :cmd:`Add Rec LoadPath` :n:`@string` as :n:`@dirpath` but for the empty
+      logical directory path.
 
 
-.. cmd:: Print LoadPath.
+.. cmd:: Remove LoadPath @string
 
-This command displays the current |Coq| loadpath.
+   This command removes the path :n:`@string` from the current |Coq| loadpath.
 
 
-Variants:
+.. cmd:: Print LoadPath
 
+   This command displays the current |Coq| loadpath.
 
-.. cmdv:: Print LoadPath @dirpath.
+   .. cmdv:: Print LoadPath @dirpath
 
-Works as ``Print LoadPath`` but displays only
-the paths that extend the :n:`@dirpath` prefix.
+      Works as :cmd:`Print LoadPath` but displays only
+      the paths that extend the :n:`@dirpath` prefix.
 
 
-.. cmd:: Add ML Path @string.
+.. cmd:: Add ML Path @string
 
-This command adds the path :n:`@string` to the current OCaml
-loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
+   This command adds the path :n:`@string` to the current OCaml
+   loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
 
 
-.. cmd:: Add Rec ML Path @string.
+.. cmd:: Add Rec ML Path @string
 
-This command adds the directory :n:`@string` and all its subdirectories to
-the current OCaml loadpath (see the command ``Declare ML Module``
-in Section :ref:`compiled-files`).
+   This command adds the directory :n:`@string` and all its subdirectories to
+   the current OCaml loadpath (see the command :cmd:`Declare ML Module`).
 
 
-.. cmd:: Print ML Path @string.
+.. cmd:: Print ML Path @string
 
-This command displays the current OCaml loadpath. This
-command makes sense only under the bytecode version of ``coqtop``, i.e.
-using option ``-byte``
-(see the command Declare ML Module in Section :ref:`compiled-files`).
+   This command displays the current OCaml loadpath. This
+   command makes sense only under the bytecode version of ``coqtop``, i.e.
+   using option ``-byte``
+   (see the command Declare ML Module in Section :ref:`compiled-files`).
 
 .. _locate-file:
 
-.. cmd:: Locate File @string.
+.. cmd:: Locate File @string
 
-This command displays the location of file string in the current
-loadpath. Typically, string is a .cmo or .vo or .v file.
+   This command displays the location of file string in the current
+   loadpath. Typically, string is a .cmo or .vo or .v file.
 
 
-.. cmd:: Locate Library @dirpath.
+.. cmd:: Locate Library @dirpath
 
-This command gives the status of the |Coq| module dirpath. It tells if
-the module is loaded and if not searches in the load path for a module
-of logical name :n:`@dirpath`.
+   This command gives the status of the |Coq| module dirpath. It tells if
+   the module is loaded and if not searches in the load path for a module
+   of logical name :n:`@dirpath`.
 
 
 .. _backtracking:
@@ -927,95 +846,71 @@ interactively, they cannot be part of a vernacular file loaded via
 ``Load`` or compiled by ``coqc``.
 
 
-.. cmd:: Reset @ident.
-
-This command removes all the objects in the environment since :n:`@ident`
-was introduced, including :n:`@ident`. :n:`@ident` may be the name of a defined or
-declared object as well as the name of a section. One cannot reset
-over the name of a module or of an object inside a module.
-
-
-Error messages:
-
-.. exn:: @ident: no such entry
-
-Variants:
-
-.. cmd:: Reset Initial.
-
-Goes back to the initial state, just after the start
-of the interactive session.
-
-
-
-.. cmd:: Back.
-
-This commands undoes all the effects of the last vernacular command.
-Commands read from a vernacular file via a ``Load`` are considered as a
-single command. Proof management commands are also handled by this
-command (see Chapter :ref:`proofhandling`). For that, Back may have to undo more than
-one command in order to reach a state where the proof management
-information is available. For instance, when the last command is a
-``Qed``, the management information about the closed proof has been
-discarded. In this case, ``Back`` will then undo all the proof steps up to
-the statement of this proof.
-
-
-Variants:
+.. cmd:: Reset @ident
 
+   This command removes all the objects in the environment since :n:`@ident`
+   was introduced, including :n:`@ident`. :n:`@ident` may be the name of a defined or
+   declared object as well as the name of a section. One cannot reset
+   over the name of a module or of an object inside a module.
 
-.. cmdv:: Back @num.
+   .. exn:: @ident: no such entry.
 
-Undoes :n:`@num` vernacular commands. As for Back, some extra
-commands may be undone in order to reach an adequate state. For
-instance Back :n:`@num` will not re-enter a closed proof, but rather go just
-before that proof.
+   .. cmdv:: Reset Initial
 
+      Goes back to the initial state, just after the start
+      of the interactive session.
 
 
-Error messages:
+.. cmd:: Back
 
+   This command undoes all the effects of the last vernacular command.
+   Commands read from a vernacular file via a :cmd:`Load` are considered as a
+   single command. Proof management commands are also handled by this
+   command (see Chapter :ref:`proofhandling`). For that, Back may have to undo more than
+   one command in order to reach a state where the proof management
+   information is available. For instance, when the last command is a
+   :cmd:`Qed`, the management information about the closed proof has been
+   discarded. In this case, :cmd:`Back` will then undo all the proof steps up to
+   the statement of this proof.
 
-.. exn:: Invalid backtrack
+   .. cmdv:: Back @num
 
-The user wants to undo more commands than available in the history.
+      Undo :n:`@num` vernacular commands. As for Back, some extra
+      commands may be undone in order to reach an adequate state. For
+      instance Back :n:`@num` will not re-enter a closed proof, but rather go just
+      before that proof.
 
-.. cmd:: BackTo @num.
+   .. exn:: Invalid backtrack.
 
-This command brings back the system to the state labeled :n:`@num`,
-forgetting the effect of all commands executed after this state. The
-state label is an integer which grows after each successful command.
-It is displayed in the prompt when in -emacs mode. Just as ``Back`` (see
-above), the ``BackTo`` command now handles proof states. For that, it may
-have to undo some extra commands and end on a state `num′ ≤ num` if
-necessary.
+      The user wants to undo more commands than available in the history.
 
+.. cmd:: BackTo @num
 
-Variants:
+   This command brings back the system to the state labeled :n:`@num`,
+   forgetting the effect of all commands executed after this state. The
+   state label is an integer which grows after each successful command.
+   It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see
+   above), the :cmd:`BackTo` command now handles proof states. For that, it may
+   have to undo some extra commands and end on a state `num′ ≤ num` if
+   necessary.
 
+   .. cmdv:: Backtrack @num @num @num
 
-.. cmdv:: Backtrack @num @num @num.
+      .. deprecated:: 8.4
 
-`Backtrack` is a *deprecated* form of
-`BackTo` which allows explicitly manipulating the proof environment. The
-three numbers represent the following:
+      :cmd:`Backtrack` is a *deprecated* form of
+      :cmd:`BackTo` which allows explicitly manipulating the proof environment. The
+      three numbers represent the following:
 
-    + *first number* : State label to reach, as for BackTo.
-    + *second number* : *Proof state number* to unbury once aborts have been done.
-      |Coq| will compute the number of Undo to perform (see Chapter :ref:`proofhandling`).
-    + *third number* : Number of Abort to perform, i.e. the number of currently
-      opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`).
+      + *first number* : State label to reach, as for :cmd:`BackTo`.
+      + *second number* : *Proof state number* to unbury once aborts have been done.
+        |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`).
+      + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently
+        opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`).
 
+   .. exn:: Invalid backtrack.
 
-
-
-Error messages:
-
-
-.. exn:: Invalid backtrack
-
-
-The destination state label is unknown.
+      The destination state label is unknown.
 
 
 .. _quitting-and-debugging:
@@ -1024,86 +919,81 @@ Quitting and debugging
 --------------------------
 
 
-.. cmd:: Quit.
-
-This command permits to quit |Coq|.
+.. cmd:: Quit
 
+   This command permits to quit |Coq|.
 
-.. cmd:: Drop.
 
-This is used mostly as a debug facility by |Coq|’s implementors and does
-not concern the casual user. This command permits to leave |Coq|
-temporarily and enter the OCaml toplevel. The OCaml
-command:
+.. cmd:: Drop
 
+   This is used mostly as a debug facility by |Coq|’s implementors and does
+   not concern the casual user. This command permits to leave |Coq|
+   temporarily and enter the OCaml toplevel. The OCaml
+   command:
 
-::
+   ::
 
-    #use "include";;
+      #use "include";;
 
+   adds the right loadpaths and loads some toplevel printers for all
+   abstract types of |Coq|- section_path, identifiers, terms, judgments, ….
+   You can also use the file base_include instead, that loads only the
+   pretty-printers for section_paths and identifiers. You can return back
+   to |Coq| with the command:
 
-adds the right loadpaths and loads some toplevel printers for all
-abstract types of |Coq|- section_path, identifiers, terms, judgments, ….
-You can also use the file base_include instead, that loads only the
-pretty-printers for section_paths and identifiers. You can return back
-to |Coq| with the command:
+   ::
 
+      go();;
 
-::
-
-    go();;
-
-.. warning::
-
-   #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`,
-      see Section `interactive-use`).
-   #. You must have compiled |Coq| from the source package and set the
-      environment variable COQTOP to the root of your copy of the sources
-      (see Section `customization-by-environment-variables`).
+   .. warning::
 
+      #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`,
+         see Section `interactive-use`).
+      #. You must have compiled |Coq| from the source package and set the
+         environment variable COQTOP to the root of your copy of the sources
+         (see Section `customization-by-environment-variables`).
 
 
 .. TODO : command is not a syntax entry
 
-.. cmd:: Time @command.
+.. cmd:: Time @command
 
-This command executes the vernacular command :n:`@command` and displays the
-time needed to execute it.
+   This command executes the vernacular command :n:`@command` and displays the
+   time needed to execute it.
 
 
-.. cmd:: Redirect @string @command.
+.. cmd:: Redirect @string @command
 
-This command executes the vernacular command :n:`@command`, redirecting its
-output to ":n:`@string`.out".
+   This command executes the vernacular command :n:`@command`, redirecting its
+   output to ":n:`@string`.out".
 
 
-.. cmd:: Timeout @num @command.
+.. cmd:: Timeout @num @command
 
-This command executes the vernacular command :n:`@command`. If the command
-has not terminated after the time specified by the :n:`@num` (time
-expressed in seconds), then it is interrupted and an error message is
-displayed.
+   This command executes the vernacular command :n:`@command`. If the command
+   has not terminated after the time specified by the :n:`@num` (time
+   expressed in seconds), then it is interrupted and an error message is
+   displayed.
 
+   .. opt:: Default Timeout @num
 
-.. opt:: Default Timeout @num
+      This option controls a default timeout for subsequent commands, as if they
+      were passed to a :cmd:`Timeout` command. Commands already starting by a
+      :cmd:`Timeout` are unaffected.
 
-   This option controls a default timeout for subsequent commands, as if they
-   were passed to a :cmd:`Timeout` command. Commands already starting by a
-   :cmd:`Timeout` are unaffected.
 
-.. cmd:: Fail @command.
+.. cmd:: Fail @command
 
-For debugging scripts, sometimes it is desirable to know
-whether a command or a tactic fails. If the given :n:`@command`
-fails, the ``Fail`` statement succeeds, without changing the proof
-state, and in interactive mode, the system
-prints a message confirming the failure.
-If the given :n:`@command` succeeds, the statement is an error, and
-it prints a message indicating that the failure did not occur.
+   For debugging scripts, sometimes it is desirable to know
+   whether a command or a tactic fails. If the given :n:`@command`
+   fails, the ``Fail`` statement succeeds, without changing the proof
+   state, and in interactive mode, the system
+   prints a message confirming the failure.
+   If the given :n:`@command` succeeds, the statement is an error, and
+   it prints a message indicating that the failure did not occur.
 
-Error messages:
+   .. exn:: The command has not failed!
 
-.. exn:: The command has not failed!
 
 .. _controlling-display:
 
@@ -1131,13 +1021,13 @@ Controlling display
    :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their
    output, printing only identifiers.
 
-.. opt:: Printing Width @integer
+.. opt:: Printing Width @num
 
    This command sets which left-aligned part of the width of the screen is used
    for display. At the time of writing this documentation, the default value
    is 78.
 
-.. opt:: Printing Depth @integer
+.. opt:: Printing Depth @num
 
    This option controls the nesting depth of the formatter used for pretty-
    printing. Beyond this depth, display of subterms is replaced by dots. At the
@@ -1181,79 +1071,77 @@ as numbers, and for reflection-based tactics. The commands to fine-
 tune the reduction strategies and the lazy conversion algorithm are
 described first.
 
-.. cmd:: Opaque {+ @qualid }.
-
-This command has an effect on unfoldable constants, i.e. on constants
-defined by ``Definition`` or ``Let`` (with an explicit body), or by a command
-assimilated to a definition such as ``Fixpoint``, ``Program Definition``, etc,
-or by a proof ended by ``Defined``. The command tells not to unfold the
-constants in the :n:`@qualid` sequence in tactics using δ-conversion (unfolding
-a constant is replacing it by its definition).
-
-``Opaque`` has also an effect on the conversion algorithm of |Coq|, telling
-it to delay the unfolding of a constant as much as possible when |Coq|
-has to check the conversion (see Section :ref:`conversion-rules`) of two distinct
-applied constants.
-
-The scope of ``Opaque`` is limited to the current section, or current
-file, unless the variant ``Global Opaque`` is used.
+.. cmd:: Opaque {+ @qualid }
 
+   This command has an effect on unfoldable constants, i.e. on constants
+   defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command
+   assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc,
+   or by a proof ended by :cmd:`Defined`. The command tells not to unfold the
+   constants in the :n:`@qualid` sequence in tactics using δ-conversion (unfolding
+   a constant is replacing it by its definition).
 
-See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
+   :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling
+   it to delay the unfolding of a constant as much as possible when |Coq|
+   has to check the conversion (see Section :ref:`conversion-rules`) of two distinct
+   applied constants.
 
+   .. cmdv:: Global Opaque {+ @qualid }
+      :name: Global Opaque
 
-Error messages:
+      The scope of :cmd:`Opaque` is limited to the current section, or current
+      file, unless the variant :cmd:`Global Opaque` is used.
 
+   See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`,
+   :ref:`proof-editing-mode`
 
-.. exn:: The reference @qualid was not found in the current environment
+   .. exn:: The reference @qualid was not found in the current environment.
 
-There is no constant referred by :n:`@qualid` in the environment.
-Nevertheless, if you asked ``Opaque`` `foo` `bar` and if `bar` does not exist, `foo` is set opaque.
+      There is no constant referred by :n:`@qualid` in the environment.
+      Nevertheless, if you asked :cmd:`Opaque` `foo` `bar` and if `bar` does
+      not exist, `foo` is set opaque.
 
-.. cmd:: Transparent {+ @qualid }.
+.. cmd:: Transparent {+ @qualid }
 
-This command is the converse of `Opaque`` and it applies on unfoldable
-constants to restore their unfoldability after an Opaque command.
+   This command is the converse of :cmd:`Opaque` and it applies on unfoldable
+   constants to restore their unfoldability after an Opaque command.
 
-Note in particular that constants defined by a proof ended by Qed are
-not unfoldable and Transparent has no effect on them. This is to keep
-with the usual mathematical practice of *proof irrelevance*: what
-matters in a mathematical development is the sequence of lemma
-statements, not their actual proofs. This distinguishes lemmas from
-the usual defined constants, whose actual values are of course
-relevant in general.
+   Note in particular that constants defined by a proof ended by Qed are
+   not unfoldable and Transparent has no effect on them. This is to keep
+   with the usual mathematical practice of *proof irrelevance*: what
+   matters in a mathematical development is the sequence of lemma
+   statements, not their actual proofs. This distinguishes lemmas from
+   the usual defined constants, whose actual values are of course
+   relevant in general.
 
-The scope of Transparent is limited to the current section, or current
-file, unless the variant ``Global Transparent`` is
-used.
+   .. cmdv:: Global Transparent {+ @qualid }
+      :name: Global Transparent
 
+      The scope of Transparent is limited to the current section, or current
+      file, unless the variant :cmd:`Global Transparent` is
+      used.
 
-Error messages:
+   .. exn:: The reference @qualid was not found in the current environment.
 
+      There is no constant referred by :n:`@qualid` in the environment.
 
-.. exn:: The reference @qualid was not found in the current environment
-
-There is no constant referred by :n:`@qualid` in the environment.
-
-
-
-See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
+   See also: sections :ref:`performingcomputations`,
+   :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
 
 .. _vernac-strategy:
 
-.. cmd:: Strategy @level [ {+ @qualid } ].
+.. cmd:: Strategy @level [ {+ @qualid } ]
 
-This command generalizes the behavior of Opaque and Transparent
-commands. It is used to fine-tune the strategy for unfolding
-constants, both at the tactic level and at the kernel level. This
-command associates a level to the qualified names in the :n:`@qualid`
-sequence. Whenever two
-expressions with two distinct head constants are compared (for
-instance, this comparison can be triggered by a type cast), the one
-with lower level is expanded first. In case of a tie, the second one
-(appearing in the cast type) is expanded.
+   This command generalizes the behavior of Opaque and Transparent
+   commands. It is used to fine-tune the strategy for unfolding
+   constants, both at the tactic level and at the kernel level. This
+   command associates a level to the qualified names in the :n:`@qualid`
+   sequence. Whenever two
+   expressions with two distinct head constants are compared (for
+   instance, this comparison can be triggered by a type cast), the one
+   with lower level is expanded first. In case of a tie, the second one
+   (appearing in the cast type) is expanded.
 
-Levels can be one of the following (higher to lower):
+   Levels can be one of the following (higher to lower):
 
     + ``opaque`` : level of opaque constants. They cannot be expanded by
       tactics (behaves like +∞, see next item).
@@ -1266,52 +1154,42 @@ Levels can be one of the following (higher to lower):
     + ``expand`` : level of constants that should be expanded first (behaves
       like −∞)
 
+    .. cmdv:: Local Strategy @level [ {+ @qualid } ]
 
-These directives survive section and module closure, unless the
-command is prefixed by Local. In the latter case, the behavior
-regarding sections and modules is the same as for the ``Transparent`` and
-``Opaque`` commands.
-
-
-.. cmd:: Print Strategy @qualid.
-
-This command prints the strategy currently associated to :n:`@qualid`. It
-fails if :n:`@qualid` is not an unfoldable reference, that is, neither a
-variable nor a constant.
-
-
-Error messages:
-
-
-.. exn:: The reference is not unfoldable.
-
-
+       These directives survive section and module closure, unless the
+       command is prefixed by ``Local``. In the latter case, the behavior
+       regarding sections and modules is the same as for the :cmd:`Transparent` and
+       :cmd:`Opaque` commands.
 
-Variants:
 
+.. cmd:: Print Strategy @qualid
 
-.. cmdv:: Print Strategies.
+   This command prints the strategy currently associated to :n:`@qualid`. It
+   fails if :n:`@qualid` is not an unfoldable reference, that is, neither a
+   variable nor a constant.
 
-Print all the currently non-transparent strategies.
+   .. exn:: The reference is not unfoldable.
 
+   .. cmdv:: Print Strategies
 
+      Print all the currently non-transparent strategies.
 
-.. cmd:: Declare Reduction @ident := @convtactic.
 
-This command allows giving a short name to a reduction expression, for
-instance lazy beta delta [foo bar]. This short name can then be used
-in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command
-accepts the
-Local modifier, for discarding this reduction name at the end of the
-file or module. For the moment the name cannot be qualified. In
-particular declaring the same name in several modules or in several
-functor applications will be refused if these declarations are not
-local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but
-nothing prevents the user to also perform a
-``Ltac`` `ident` ``:=`` `convtactic`.
+.. cmd:: Declare Reduction @ident := @convtactic
 
+   This command allows giving a short name to a reduction expression, for
+   instance lazy beta delta [foo bar]. This short name can then be used
+   in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command
+   accepts the
+   Local modifier, for discarding this reduction name at the end of the
+   file or module. For the moment the name cannot be qualified. In
+   particular declaring the same name in several modules or in several
+   functor applications will be refused if these declarations are not
+   local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but
+   nothing prevents the user to also perform a
+   ``Ltac`` `ident` ``:=`` `convtactic`.
 
-See also: sections :ref:`performingcomputations`
+   See also: sections :ref:`performingcomputations`
 
 
 .. _controlling-locality-of-commands:
@@ -1320,8 +1198,8 @@ Controlling the locality of commands
 -----------------------------------------
 
 
-.. cmd:: Local @command.
-.. cmd:: Global @command.
+.. cmd:: Local @command
+.. cmd:: Global @command
 
 Some commands support a Local or Global prefix modifier to control the
 scope of their effect. There are four kinds of commands:
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index c4a7121ce4..6958b5f265 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -200,7 +200,7 @@ need to force the parsing level of y, as follows.
 For the sake of factorization with Coq predefined rules, simple rules
 have to be observed for notations starting with a symbol: e.g. rules
 starting with “{” or “(” should be put at level 0. The list of Coq
-predefined notations can be found in Chapter 3.
+predefined notations can be found in Chapter :ref:`thecoqlibrary`.
 
 .. cmd:: Print Grammar constr.