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

10 files changed, 258 insertions, 267 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