[Sphinx] Clean-up indices

5 files changed, 398 insertions, 267 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 247d5d899..009758319 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -178,6 +178,7 @@ Sequence
 A sequence is an expression of the following form:
 
 .. tacn:: @expr ; @expr
+   :name: ;
 
    The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be
    a tactic value. The tactic :n:`v__1` is applied to the current goal,
@@ -193,6 +194,7 @@ Different tactics can be applied to the different goals using the
 following form:
 
 .. tacn:: [> {*| @expr }]
+   :name: [> ... | ... | ... ] (dispatch)
 
    The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for
    i=0,...,n and all have to be tactics. The :n:`v__i` is applied to the
@@ -240,6 +242,7 @@ We can restrict the application of a tactic to a subset of the currently
 focused goals with:
 
 .. tacn:: @toplevel_selector : @expr
+   :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``:
@@ -290,6 +293,7 @@ For loop
 There is a for loop that repeats a tactic :token:`num` times:
 
 .. tacn:: do @num @expr
+   :name: do
 
    :n:`@expr` is evaluated to ``v`` which must be a tactic value. This tactic
    value ``v`` is applied :token:`num` times. Supposing :token:`num` > 1, after the
@@ -303,6 +307,7 @@ Repeat loop
 We have a repeat loop with:
 
 .. tacn:: repeat @expr
+   :name: repeat
 
    :n:`@expr` is evaluated to ``v``. If ``v`` denotes a tactic, this tactic is
    applied to each focused goal independently. If the application succeeds, the
@@ -316,6 +321,7 @@ Error catching
 We can catch the tactic errors with:
 
 .. tacn:: try @expr
+   :name: try
 
    :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic
    value ``v`` is applied to each focused goal independently. If the application of
@@ -329,6 +335,7 @@ Detecting progress
 We can check if a tactic made progress with:
 
 .. tacn:: progress expr
+   :name: progress
 
    :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v``
    is applied to each focued subgoal independently. If the application of ``v``
@@ -343,6 +350,7 @@ Backtracking branching
 We can branch with the following structure:
 
 .. tacn:: @expr__1 + @expr__2
+   :name: + (backtracking branching)
 
    :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and
    :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is applied to
@@ -365,6 +373,7 @@ restrict to a local, left biased, branching and consider the first
 tactic to work (i.e. which does not fail) among a panel of tactics:
 
 .. tacn:: first [{*| @expr}]
+   :name: first
 
    The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be
    tactic values, for i=1,...,n. Supposing n>1, it applies, in each focused
@@ -396,6 +405,7 @@ Yet another way of branching without backtracking is the following
 structure:
 
 .. tacn:: @expr__1 || @expr__2
+   :name: || (left-biased branching)
 
    :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and
    :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is
@@ -410,6 +420,7 @@ Generalized biased branching
 The tactic
 
 .. tacn:: tryif @expr__1 then @expr__2 else @expr__3
+   :name: tryif
 
    is a generalization of the biased-branching tactics above. The
    expression :n:`@expr__1` is evaluated to :n:`v__1`, which is then
@@ -430,6 +441,7 @@ Another way of restricting backtracking is to restrict a tactic to a
 single success *a posteriori*:
 
 .. tacn:: once @expr
+   :name: once
 
    :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied but only its first success is used. If ``v`` fails,
@@ -443,6 +455,7 @@ Coq provides an experimental way to check that a tactic has *exactly
 one* success:
 
 .. tacn:: exactly_once @expr
+   :name: exactly_once
 
    :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied if it has at most one success. If ``v`` fails,
@@ -467,6 +480,7 @@ Checking the failure
 Coq provides a derived tactic to check that a tactic *fails*:
 
 .. tacn:: assert_fails @expr
+   :name: assert_fails
 
    This behaves like :n:`tryif @expr then fail 0 tac "succeeds" else idtac`.
 
@@ -477,6 +491,7 @@ Coq provides a derived tactic to check that a tactic has *at least one*
 success:
 
 .. tacn:: assert_succeeds @expr
+   :name: assert_suceeds
 
    This behaves like
    :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`.
@@ -488,6 +503,7 @@ We may consider the first to solve (i.e. which generates no subgoal)
 among a panel of tactics:
 
 .. tacn:: solve [{*| @expr}]
+   :name: solve
 
    The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be
    tactic values, for i=1,...,n. Supposing n>1, it applies :n:`v__1` to
@@ -508,6 +524,7 @@ The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but
 it appears in the proof script.
 
 .. tacn:: idtac {* message_token}
+   :name: idtac
 
    This prints the given tokens. Strings and integers are printed
    literally. If a (term) variable is given, its contents are printed.
@@ -516,6 +533,7 @@ Failing
 ~~~~~~~
 
 .. tacn:: fail
+   :name: fail
 
    This is the always-failing tactic: it does not solve any
    goal. It is useful for defining other tacticals since it can be caught by
@@ -543,6 +561,7 @@ Failing
       This is a combination of the previous variants.
 
    .. tacv:: gfail
+      :name: gfail
 
       This variant fails even if there are no goals left.
 
@@ -565,6 +584,7 @@ We can force a tactic to stop if it has not finished after a certain
 amount of time:
 
 .. tacn:: timeout @num @expr
+   :name: timeout
 
    :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied normally, except that it is interrupted after :n:`@num` seconds
@@ -586,6 +606,7 @@ Timing a tactic
 A tactic execution can be timed:
 
 .. tacn:: time @string @expr
+   :name: time
 
    evaluates :n:`@expr` and displays the time the tactic expression ran, whether it
    fails or successes. In case of several successes, the time for each successive
@@ -600,6 +621,7 @@ Tactic expressions that produce terms can be timed with the experimental
 tactic
 
 .. tacn:: time_constr expr
+   :name: time_constr
 
    which evaluates :n:`@expr ()` and displays the time the tactic expression
    evaluated, assuming successful evaluation. Time is in seconds and is
@@ -610,10 +632,12 @@ tactic
    implemented using the tactics
 
    .. tacn:: restart_timer @string
+      :name: restart_timer
 
    and
 
    .. tacn:: finish_timing {? @string} @string
+      :name: finish_timing
 
    which (re)set and display an optionally named timer, respectively. The
    parenthesized string argument to :n:`finish_timing` is also optional, and
@@ -951,6 +975,7 @@ Testing boolean expressions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. tacn:: guard @test
+   :name: guard
 
    The :tacn:`guard` tactic tests a boolean expression, and fails if the expression
    evaluates to false. If the expression evaluates to true, it succeeds
@@ -976,6 +1001,7 @@ Proving a subgoal as a separate lemma
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. tacn:: abstract @expr
+   :name: abstract
 
    From the outside, :n:`abstract @expr` is the same as :n:`solve @expr`.
    Internally it saves an auxiliary lemma called ``ident_subproofn`` where
@@ -1000,6 +1026,7 @@ Proving a subgoal as a separate lemma
          don’t play well with asynchronous proofs.
 
    .. tacv:: transparent_abstract @expr
+      :name: transparent_abstract
 
       Save the subproof in a transparent lemma rather than an opaque one.
 
@@ -1220,28 +1247,33 @@ performance bug.
    Unset Ltac Profiling.
 
 .. tacn:: start ltac profiling
+   :name: start ltac profiling
 
    This tactic behaves like :tacn:`idtac` but enables the profiler.
 
 .. tacn:: stop ltac profiling
+   :name: stop ltac profiling
 
    Similarly to :tacn:`start ltac profiling`, this tactic behaves like
    :tacn:`idtac`. Together, they allow you to exclude parts of a proof script
    from profiling.
 
 .. tacn:: reset ltac profile
+   :name: reset ltac profile
 
    This tactic behaves like the corresponding vernacular command
    and allow displaying and resetting the profile from tactic scripts for
    benchmarking purposes.
 
 .. tacn:: show ltac profile
+   :name: show ltac profile
 
    This tactic behaves like the corresponding vernacular command
    and allow displaying and resetting the profile from tactic scripts for
    benchmarking purposes.
 
 .. tacn:: show ltac profile @string
+   :name: show ltac profile
 
    This tactic behaves like the corresponding vernacular command
    and allow displaying and resetting the profile from tactic scripts for
@@ -1261,6 +1293,7 @@ Run-time optimization tactic
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. tacn:: optimize_heap
+   :name: optimize_heap
 
 This tactic behaves like :n:`idtac`, except that running it compacts the
 heap in the OCaml run-time system. It is analogous to the Vernacular
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index a77b127eb..86c94bab3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -58,13 +58,14 @@ statement is eventually completed and validated, the statement is then
 bound to the name ``Unnamed_thm`` (or a variant of this name not already
 used for another statement).
 
-.. cmd:: Qed.
+.. cmd:: Qed
+   :name: Qed (interactive proof)
 
 This command is available in interactive editing proof mode when the
 proof is completed. Then ``Qed`` extracts a proof term from the proof
 script, switches back to Coq top-level and attaches the extracted
 proof term to the declared name of the original goal. This name is
-added to the environment as an ``Opaque`` constant.
+added to the environment as an opaque constant.
 
 
 .. exn:: Attempt to save an incomplete proof
@@ -81,6 +82,7 @@ a while when the proof is large. In some exceptional cases one may
 even incur a memory overflow.
 
 .. cmdv:: Defined.
+   :name: Defined (interactive proof)
 
 Defines the proved term as a transparent constant.
 
@@ -91,6 +93,7 @@ command (and the following ones) can only be used if the original goal
 has been opened using the ``Goal`` command.
 
 .. cmd:: Admitted.
+   :name: Admitted (interactive proof)
 
 This command is available in interactive editing proof mode to give up
 the current proof and declare the initial goal as an axiom.
@@ -105,8 +108,8 @@ This command applies in proof editing mode. It is equivalent to
 That is, you have to give the full proof in one gulp, as a
 proof term (see Section :ref:`applyingtheorems`).
 
-
 .. cmdv:: Proof.
+   :name: Proof (interactive proof)
 
 Is a noop which is useful to delimit the sequence of tactic commands
 which start a proof, after a ``Theorem`` command. It is a good practice to
@@ -182,49 +185,51 @@ Proof using options
 The following options modify the behavior of ``Proof using``.
 
 
-.. cmdv:: Set 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``.
+   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``.
 
 
-.. cmdv:: Set Suggest Proof Using.
+.. opt:: Suggest Proof Using.
 
-When ``Qed`` is performed, suggest a using annotation if the user did not
-provide one.
+   When ``Qed`` is performed, suggest a using annotation if the user did not
+   provide one.
 
 ..  _`nameaset`:
 
 Name a set of section hypotheses for ``Proof using``
 ````````````````````````````````````````````````````
 
+.. cmd:: Collection @ident := @section_subset_expr
+
 The command ``Collection`` can be used to name a set of section
 hypotheses, with the purpose of making ``Proof using`` annotations more
 compact.
 
 
-.. cmdv:: Collection Some := x y z.
+.. cmdv:: Collection Some := x y z
 
 Define the collection named "Some" containing ``x``, ``y`` and ``z``.
 
 
-.. cmdv:: Collection Fewer := Some - z.
+.. cmdv:: Collection Fewer := Some - z
 
 Define the collection named "Fewer" containing only ``x`` and ``y``.
 
 
-.. cmdv::  Collection Many := Fewer + Some.
-.. cmdv::  Collection Many := Fewer - Some.
+.. cmdv::  Collection Many := Fewer + Some
+.. cmdv::  Collection Many := Fewer - Some
 
 Define the collection named "Many" containing the set union or set
 difference of "Fewer" and "Some".
 
 
-.. cmdv:: Collection Many := Fewer - (x y).
+.. cmdv:: Collection Many := Fewer - (x y)
 
 Define the collection named "Many" containing the set difference of
-"Fewer" and the unnamed collection ``x`` ``y``.
+"Fewer" and the unnamed collection ``x`` ``y``
 
 
 .. cmd:: Abort.
@@ -288,6 +293,7 @@ backtracks one step.
 Repeats Undo :n:`@num` times.
 
 .. cmdv:: Restart.
+   :name: Restart
 
 This command restores the proof editing process to the original goal.
 
@@ -424,11 +430,11 @@ Set Bullet Behavior
 
 The bullet behavior can be controlled by the following commands.
 
-.. opt:: Bullet Behavior "None".
+.. opt:: Bullet Behavior "None"
 
 This makes bullets inactive.
 
-.. opt:: Bullet Behavior "Strict Subproofs".
+.. opt:: Bullet Behavior "Strict Subproofs"
 
 This makes bullets active (this is the default behavior).
 
@@ -551,7 +557,7 @@ Controlling the effect of proof editing commands
 ------------------------------------------------
 
 
-.. opt:: Hyps Limit @num.
+.. opt:: Hyps Limit @num
 
 This option controls the maximum number of hypotheses displayed in goals
 after the application of a tactic. All the hypotheses remain usable
@@ -560,7 +566,7 @@ When unset, it goes back to the default mode which is to print all
 available hypotheses.
 
 
-.. opt:: Automatic Introduction.
+.. opt:: Automatic Introduction
 
 This option controls the way binders are handled
 in assertion commands such as ``Theorem ident [binders] : form``. When the
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 6ddb0b027..977a5b8fa 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -493,7 +493,10 @@ inferred from the whole context of the goal (see for example section
 Definitions
 ~~~~~~~~~~~
 
-The pose tactic allows to add a defined constant to a proof context.
+.. tacn:: pose
+   :name: pose (ssreflect)
+
+This tactic allows to add a defined constant to a proof context.
 |SSR| generalizes this tactic in several ways. In particular, the
 |SSR| pose tactic supports *open syntax*: the body of the
 definition does not need surrounding parentheses. For instance:
@@ -1349,6 +1352,7 @@ Discharge
 The general syntax of the discharging tactical ``:`` is:
 
 .. tacn:: @tactic {? @ident } : {+ @d_item } {? @clear_switch }
+   :name: ... : ... (ssreflect)
 
 .. prodn::
    d_item ::= {? @occ_switch %| @clear_switch } @term
@@ -1500,9 +1504,11 @@ side of an equation.
 The abstract tactic
 ```````````````````
 
-The ``abstract`` tactic assigns an ``abstract`` constant previously
-introduced with the ``[: name ]`` intro pattern
-(see section :ref:`introduction_ssr`).
+.. tacn:: abstract: {+ d_item}
+   :name abstract (ssreflect)
+
+This tactic assigns an abstract constant previously introduced with the ``[:
+name ]`` intro pattern (see section :ref:`introduction_ssr`).
 
 In a goal like the following::
 
@@ -1809,6 +1815,8 @@ of a :token:`d_item` immediately following this ``/`` switch,
 using the syntax:
 
 .. tacv:: case: {+ @d_item } / {+ @d_item }
+   :name: case (ssreflect)
+
 .. tacv:: elim: {+ @d_item } / {+ @d_item }
 
 The :token:`d_item` on the right side of the ``/`` switch are discharged as
@@ -2132,7 +2140,7 @@ tactic using the given second tactic, and fails if it does not succeed.
 Its analogue
 
 .. tacn:: @tactic ; first by @tactic
-   :name: first
+   :name: first (ssreflect)
 
 tries to solve the first subgoal generated by the first tactic using the
 second given tactic, and fails if it does not succeed.
@@ -2212,7 +2220,7 @@ Iteration
 thanks to the do tactical, whose general syntax is:
 
 .. tacn:: do {? @mult } ( @tactic | [ {+| @tactic } ] )
-   :name: do
+   :name: do (ssreflect)
 
 where :token:`mult` is a *multiplier*.
 
@@ -3724,6 +3732,7 @@ We provide a special tactic unlock for unfolding such definitions
 while removing “locks”, e.g., the tactic:
 
 .. tacn:: unlock {? @occ_switch } @ident
+   :name: unlock
 
 replaces the occurrence(s) of :token:`ident` coded by the
 :token:`occ_switch` with the corresponding body.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 1868f4b9d..7a45272f2 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -51,7 +51,7 @@ specified, the default selector is used.
      tactic_invocation : toplevel_selector : tactic.
                        : |tactic .
 
-.. opt:: Default Goal Selector @toplevel_selector.
+.. opt:: Default Goal Selector @toplevel_selector
 
    This option controls the default selector – used when no selector is
    specified when applying a tactic – is set to the chosen value. The initial
@@ -168,6 +168,7 @@ term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then
 .. exn:: Not an exact proof.
 
 .. tacv:: eexact @term.
+   :name: eexact
 
 This tactic behaves like exact but is able to handle terms and goals with
 meta-variables.
@@ -181,6 +182,7 @@ the goal. If it is the case, the subgoal is proved. Otherwise, it fails.
 .. exn:: No such assumption.
 
 .. tacv:: eassumption
+   :name: eassumption
 
 This tactic behaves like assumption but is able to handle goals with
 meta-variables.
@@ -233,6 +235,7 @@ useful to advanced users.
    cast around it.
 
 .. 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.
@@ -243,6 +246,7 @@ useful to advanced users.
    resolution of typeclasses.
 
 .. tacv:: simple notypeclasses refine @term
+   :name: simple notypeclasses refine
 
    This tactic behaves like ``simple refine`` except it performs typechecking
    without resolution of typeclasses.
@@ -313,6 +317,7 @@ instantiate (see :ref:`Existential-Variables`). The instantiation is
 intended to be found later in the proof.
 
 .. 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
@@ -335,6 +340,7 @@ does.
 
 .. 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``.
 
@@ -515,8 +521,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
 
@@ -534,34 +540,39 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
     The terms in the @bindings_list are checked in the context where constructor is executed and not in the context where @apply is executed (the introductions are not taken into account).
 
 .. tacv:: split
+   :name: split
 
    This applies only if :g:`I` has a single constructor. It is then
    equivalent to :n:`constructor 1.`. It is typically used in the case of a
    conjunction :g:`A` :math:`\wedge` :g:`B`.
 
-.. exn:: Not an inductive goal with 1 constructor.
+.. exn:: Not an inductive goal with 1 constructor
 
 .. tacv:: exists @val
+   :name: exists
 
    This applies only if :g:`I` has a single constructor. It is then equivalent
    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
 
    This iteratively applies :n:`exists @bindings_list`.
 
 .. tacv:: left
+   :name: left
+
 .. tacv:: right
+   :name: right
 
    These tactics apply only if :g:`I` has two constructors, for
    instance in the case of a disjunction :g:`A` :math:`\vee` :g:`B`.
    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
@@ -572,15 +583,25 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    for the appropriate ``i``.
 
 .. tacv:: econstructor
+   :name: econstructor
+
 .. tacv:: eexists
+   :name: eexists
+
 .. tacv:: esplit
+   :name: esplit
+
 .. tacv:: eleft
+   :name: eleft
+
 .. tacv:: eright
+   :name: eright
 
-   These tactics and their variants behave like ``constructor``, ``exists``,
-   ``split``, ``left``, ``right`` and their variants but they introduce
-   existential variables instead of failing when the instantiation of a
-   variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`).
+   These tactics and their variants behave like :tacn:`constructor`,
+   :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their variants
+   but they introduce existential variables instead of failing when the
+   instantiation of a variable cannot be found (cf. :tacn:`eapply` and
+   :tacn:`apply`).
 
 
 .. _managingthelocalcontext:
@@ -611,7 +632,7 @@ the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can
 be applied or the goal is not head-reducible.
 
 .. exn:: No product even after head-reduction.
-.. exn:: ident is already used.
+.. exn:: @ident is already used.
 
 .. tacv:: intros
 
@@ -845,6 +866,7 @@ quantification or an implication.
    This is equivalent to :n:`clear @ident. ... clear @ident.`
 
 .. tacv:: clearbody @ident
+   :name: clearbody
 
    This tactic expects :n:`@ident` to be a local definition then clears its
    body. Otherwise said, this tactic turns a definition into an assumption.
@@ -866,7 +888,7 @@ quantification or an implication.
    it.
 
 .. tacn:: revert {+ @ident}
-   :name: revert ...
+   :name: revert
 
 This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses
 (possibly defined) to the goal, if this respects dependencies. This tactic is
@@ -982,6 +1004,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
 
 .. tacv:: eset (@ident {+ @binder} := @term ) in @goal_occurrences
 .. tacv:: eset @term in @goal_occurrences
+   :name: eset
 
    While the different variants of :tacn:`set` expect that no existential
    variables are generated by the tactic, :n:`eset` removes this constraint. In
@@ -989,6 +1012,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    :tacn:`epose`, i.e. when the :`@term` does not occur in the goal.
 
 .. tacv:: remember @term as @ident
+   :name: remember
 
    This behaves as :n:`set (@ident:= @term ) in *` and using a logical
    (Leibniz’s) equality instead of a local definition.
@@ -1006,6 +1030,8 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
 .. tacv:: eremember @term as @ident
 .. tacv:: eremember @term as @ident in @goal_occurrences
 .. tacv:: eremember @term as @ident eqn:@ident
+   :name: eremember
+
    While the different variants of :n:`remember` expect that no existential
    variables are generated by the tactic, :n:`eremember` removes this constraint.
 
@@ -1112,6 +1138,7 @@ Controlling the proof flow
    .. exn:: Variable @ident is already declared
 
 .. tacv:: eassert form as intro_pattern by tactic
+   :name: eassert
 
 .. tacv:: assert (@ident := @term)
 
@@ -1121,6 +1148,7 @@ Controlling the proof flow
    to prove it.
 
 .. tacv:: pose proof @term {? as intro_pattern}
+   :name: pose proof
 
    This tactic behaves like :n:`assert T {? as intro_pattern} by exact @term`
    where :g:`T` is the type of :g:`term`. In particular,
@@ -1134,6 +1162,7 @@ Controlling the proof flow
    the tactic, :n:`epose proof` removes this constraint.
 
 .. tacv:: enough (@ident : form)
+   :name: enough
 
    This adds a new hypothesis of name :n:`@ident` asserting :n:`form` to the
    goal the tactic :n:`enough` is applied to. A new subgoal stating :n:`form` is
@@ -1159,13 +1188,17 @@ Controlling the proof flow
    applied to all of them.
 
 .. tacv:: eenough (@ident : form) by tactic
+   :name: eenough
+
 .. tacv:: eenough form by tactic
+
 .. tacv:: eenough form as intro_pattern by tactic
 
    While the different variants of :n:`enough` expect that no existential
    variables are generated by the tactic, :n:`eenough` removes this constraint.
 
-.. tacv:: cut form
+.. tacv:: cut @form
+   :name: cut
 
    This tactic applies to any goal. It implements the non-dependent case of
    the “App” rule given in :ref:`typing-rules`. (This is Modus Ponens inference
@@ -1175,6 +1208,7 @@ Controlling the proof flow
 
 .. tacv:: specialize (ident {* @term}) {? as intro_pattern}
 .. tacv:: specialize ident with @bindings_list {? as intro_pattern}
+   :name: specialize
 
    The tactic :n:`specialize` works on local hypothesis :n:`@ident`. The
    premises of this hypothesis (either universal quantifications or
@@ -1416,6 +1450,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    dependent premises of the type of :n:`@term` (see :ref:`syntax of bindings <bindingslist>`).
 
 .. tacv:: edestruct @term
+   :name: edestruct
 
    This tactic behaves like :n:`destruct @term` except that it does not fail if
    the instance of a dependent premises of the type of :n:`@term` is not
@@ -1442,6 +1477,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    the effects of the `with`, `as`, `eqn:`, `using`, and `in` clauses.
 
 .. tacv:: case term
+   :name: case
 
    The tactic :n:`case` is a more basic tactic to perform case analysis without
    recursion. It behaves as :n:`elim @term` but using a case-analysis
@@ -1451,14 +1487,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 
    Analogous to :n:`elim @term with @bindings_list` above.
 
-.. tacv:: ecase @term
-.. tacv:: ecase @term with @bindings_list
+.. tacv:: ecase @term {? with @bindings_list }
+   :name: ecase
 
    In case the type of :n:`@term` has dependent premises, or dependent premises
    whose values are not inferable from the :n:`with @bindings_list` clause,
    :n:`ecase` turns them into existential variables to be resolved later on.
 
 .. tacv:: simple destruct @ident
+   :name: simple destruct
 
    This tactic behaves as :n:`intros until @ident; case @ident` when :n:`@ident`
    is a quantified variable of the goal.
@@ -1549,6 +1586,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    premises of the type of :n:`term` (see :ref:`bindings list <bindingslist>`).
 
 .. tacv:: einduction @term
+   :name: einduction
 
    This tactic behaves like :tacn:`induction` except that it does not fail if
    some dependent premise of the type of :n:`@term` is not inferable. Instead,
@@ -1621,6 +1659,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    (see :ref:`bindings list <bindingslist>`).
 
 .. tacv:: eelim @term
+   :name: eelim
 
    In case the type of :n:`@term` has dependent premises, this turns them into
    existential variables to be resolved later on.
@@ -1639,7 +1678,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    These are the most general forms of ``elim`` and ``eelim``. It combines the
    effects of the ``using`` clause and of the two uses of the ``with`` clause.
 
-.. tacv:: elimtype form
+.. tacv:: elimtype @form
+   :name: elimtype
 
    The argument :n:`form` must be inductively defined. :n:`elimtype I` is
    equivalent to :n:`cut I. intro Hn; elim Hn; clear Hn.` Therefore the
@@ -1649,6 +1689,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    :n:`elimtype I; 2:exact t.`
 
 .. tacv:: simple induction @ident
+   :name: simple induction
 
    This tactic behaves as :n:`intros until @ident; elim @ident` when
    :n:`@ident` is a quantified variable of the goal.
@@ -1733,6 +1774,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    other ones need not be further generalized.
 
 .. tacv:: dependent destruction @ident
+   :name: dependent destruction
 
    This performs the generalization of the instance :n:`@ident` but uses
    ``destruct`` instead of induction on the generalized hypothesis. This gives
@@ -1842,6 +1884,7 @@ See also: :ref:`advanced-recursive-functions`
 
 .. tacv:: ediscriminate @num
 .. tacv:: ediscriminate @term {? with @bindings_list}
+   :name: ediscriminate
 
    This works the same as ``discriminate`` but if the type of :n:`@term`, or the
    type of the hypothesis referred to by :n:`@num`, has uninstantiated
@@ -1921,6 +1964,7 @@ the use of a sigma type is avoided.
 
 .. tacv:: einjection @num
 .. tacv:: einjection @term {? with @bindings_list}
+   :name: einjection
 
    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
@@ -1948,17 +1992,19 @@ the use of a sigma type is avoided.
    to the number of new equalities. The original equality is erased if it
    corresponds to an hypothesis.
 
-It is possible to 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). To obtain this
-behavior, the option :opt:`Structural Injection` must be activated. This
-option is off by default.
+.. 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.
 
-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 behavior can be
-turned off by setting the option :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.
 
 .. tacn:: inversion @ident
    :name: inversion
@@ -2110,6 +2156,7 @@ turned off by setting the option :opt:`Keep Proof Equalities`.
    :n:`dependent inversion_clear @ident with @term`.
 
 .. tacv:: simple inversion @ident
+   :name: simple inversion
 
    It is a very primitive inversion tactic that derives all the necessary
    equalities but it does not simplify the constraints as ``inversion`` does.
@@ -2410,6 +2457,7 @@ subgoals.
     leading to failure if these n rewrites are not possible.
 
 .. tacv:: erewrite @term
+   :name: erewrite
 
   This tactic works as :n:`rewrite @term` but turning
   unresolved bindings into existential variables, if any, instead of
@@ -2456,6 +2504,7 @@ subgoals.
   clause argument must not contain any type of nor value of.
 
 .. tacv:: cutrewrite <- (@term = @term)
+   :cutrewrite:
 
   This tactic is deprecated. It acts like :n:`replace @term with @term`, or,
   equivalently as :n:`enough (@term = @term) as <-`.
@@ -2499,30 +2548,30 @@ unfolded and cleared.
    context for which an equality of the form :n:`@ident = t` or :n:`t = @ident`
    or :n:`@ident := t` exists, with :n:`@ident` not occurring in `t`.
 
-     ..  note::
 
-         The behavior of subst can be controlled using option :opt:`Regular Subst
-         Tactic`. When this option is activated, subst also deals with the
-         following corner cases:
+   .. opt:: Regular Subst Tactic
+
+      This option controls the behavior of :tacn:`subst`. When it is
+      activated, :tacn:`subst` also deals with the following corner cases:
 
-         + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2`
-           and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not
-           a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u`
-           or :n:`u = @ident`:sub:`2`; without the option, a second call to
-           subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or
-           `t′` respectively.
-         + The presence of a recursive equation which without the option would
-           be a cause of failure of :tacn:`subst`.
-         + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2`
-           and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the
-           option would be a cause of failure of :tacn:`subst`.
+      + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2`
+        and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not
+        a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u`
+        or :n:`u = @ident`:sub:`2`; without the option, a second call to
+        subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or
+        `t′` respectively.
+      + The presence of a recursive equation which without the option would
+        be a cause of failure of :tacn:`subst`.
+      + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2`
+        and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the
+        option would be a cause of failure of :tacn:`subst`.
 
-         Additionally, it prevents a local definition such as :n:`@ident := t` to be
-         unfolded which otherwise it would exceptionally unfold in configurations
-         containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident`
-         with `u′` not a variable. Finally, it preserves the initial order of
-         hypotheses, which without the option it may break. The option is on by
-         default.
+      Additionally, it prevents a local definition such as :n:`@ident := t` to be
+      unfolded which otherwise it would exceptionally unfold in configurations
+      containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident`
+      with `u′` not a variable. Finally, it preserves the initial order of
+      hypotheses, which without the option it may break. The option is on by
+      default.
 
 
 .. tacn:: stepl @term
@@ -2536,30 +2585,37 @@ where `eq` is typically a setoid equality. The application of :n:`stepl @term`
 then replaces the goal by :n:`R @term @term` and adds a new goal stating
 :n:`eq @term @term`.
 
-Lemmas are added to the database using the command ``Declare Left Step @term.``
+.. cmd:: Declare Left Step @term
+
+   Adds :n:`@term` to the database used by :tacn:`stepl`.
+
 The tactic is especially useful for parametric setoids which are not accepted
 as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
 :ref:`Generalizedrewriting`).
 
 .. tacv:: stepl @term by tactic
 
-  This applies :n:`stepl @term` then applies tactic to the second goal.
+   This applies :n:`stepl @term` then applies tactic to the second goal.
 
 .. tacv:: stepr @term stepr @term by tactic
+   :name: stepr
+
+   This behaves as :tacn:`stepl` but on the right-hand-side of the binary
+   relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq
+   y z -> R x z`.
 
-  This behaves as :tacn:`stepl` but on the right-hand-side of the binary
-  relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq
-  y z -> R x z` and are registered using the command ``Declare Right Step
-  @term.``
+    .. cmd:: Declare Right Step @term
+
+       Adds :n:`@term` to the database used by :tacn:`stepr`.
 
 
 .. tacn:: change @term
    :name: change
 
-  This tactic applies to any goal. It implements the rule ``Conv`` given in
-  :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T`
-  with `U` providing that `U` is well-formed and that `T` and `U` are
-  convertible.
+   This tactic applies to any goal. It implements the rule ``Conv`` given in
+   :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T`
+   with `U` providing that `U` is well-formed and that `T` and `U` are
+   convertible.
 
 .. exn:: Not convertible
 
@@ -2697,6 +2753,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    and :n:`lazy beta delta -{+ @qualid} iota zeta`.
 
 .. tacv:: vm_compute
+   :name: vm_compute
 
    This tactic evaluates the goal using the optimized call-by-value evaluation
    bytecode-based virtual machine described in :cite:`CompiledStrongReduction`.
@@ -2706,6 +2763,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    reflection-based tactics.
 
 .. tacv:: native_compute
+   :name: native_compute
 
    This tactic evaluates the goal by compilation to Objective Caml as described
    in :cite:`FullReduction`. If Coq is running in native code, it can be
@@ -3096,7 +3154,7 @@ the :tacn:`auto` and :tacn:`trivial` tactics:
 .. opt:: Info Auto
 .. opt:: Debug Auto
 .. opt:: Info Trivial
-.. opt:: Info Trivial
+.. opt:: Debug Trivial
 
 See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
@@ -3251,188 +3309,203 @@ observationally different from the legacy one.
 
 The general command to add a hint to some databases :n:`{+ @ident}` is
 
-.. cmd:: Hint hint_definition : {+ @ident}
+.. cmd:: Hint @hint_definition : {+ @ident}
 
-**Variants:**
+   .. cmdv:: Hint @hint_definition
 
-.. cmd:: Hint hint_definition
+      No database name is given: the hint is registered in the core database.
 
-   No database name is given: the hint is registered in the core database.
+   .. cmdv:: Local Hint @hint_definition : {+ @ident}
 
-.. cmd:: Local Hint hint_definition : {+ @ident}
+      This is used to declare hints that must not be exported to the other modules
+      that require and import the current module. Inside a section, the option
+      Local is useless since hints do not survive anyway to the closure of
+      sections.
 
-   This is used to declare hints that must not be exported to the other modules
-   that require and import the current module. Inside a section, the option
-   Local is useless since hints do not survive anyway to the closure of
-   sections.
+   .. cmdv:: Local Hint @hint_definition
 
-.. cmd:: Local Hint hint_definition
+      Idem for the core database.
 
-   Idem for the core database.
+   .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}}
+      :name: Hint Resolve
 
-The ``hint_definition`` is one of the following expressions:
+   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.
 
-+ :n:`Resolve @term {? | {? @num} {? @pattern}}`
-  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 ``eauto`` is a transitivity lemma.
+   .. exn:: @term cannot be used as a hint
 
-  .. exn:: @term cannot be used as a hint
+      The head symbol of the type of :n:`@term` is a bound variable such that
+      this tactic cannot be associated to a constant.
 
-     The head symbol of the type of :n:`@term` is a bound variable such that
-     this tactic cannot be associated to a constant.
+   .. cmdv:: Hint Resolve {+ @term}
 
-  **Variants:**
+      Adds each :n:`Hint Resolve @term`.
 
-   + :n:`Resolve {+ @term}`
-     Adds each :n:`Resolve @term`.
+   .. cmdv:: Hint Resolve -> @term
 
-   + :n:`Resolve -> @term`
-     Adds the left-to-right implication of an equivalence as a hint (informally
-     the hint will be used as :n:`apply <- @term`, although as mentionned
-     before, the tactic actually used is a restricted version of ``apply``).
+      Adds the left-to-right implication of an equivalence as a hint (informally
+      the hint will be used as :n:`apply <- @term`, although as mentionned
+      before, the tactic actually used is a restricted version of
+      :tacn:`apply`).
 
-   + :n:`Resolve <- @term`
-     Adds the right-to-left implication of an equivalence  as a hint.
+   .. cmdv:: Resolve <- @term
 
-+ :n:`Immediate @term`
-  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
-  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
-  never generates subgoals) is always 1, so that it is not used by ``trivial``
-  itself.
+      Adds the right-to-left implication of an equivalence  as a hint.
 
-  .. exn:: @term cannot be used as a hint
+   .. cmdv:: Hint Immediate @term
+      :name: Hint Immediate
 
-  **Variants:**
+      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
+      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
+      never generates subgoals) is always 1, so that it is not used by :tacn:`trivial`
+      itself.
 
-  + :n:`Immediate {+ @term}`
-    Adds each :n:`Immediate @term`.
+   .. exn:: @term cannot be used as a hint
 
-+ :n:`Constructors @ident`
-  If :n:`@ident` is an inductive type, this command adds all its constructors as
-  hints of type Resolve. Then, when the conclusion of current goal has the form
-  :n:`(@ident ...)`, ``auto`` will try to apply each constructor.
+   .. cmdv:: Immediate {+ @term}
 
-  .. exn:: @ident is not an inductive type
+      Adds each :n:`Hint Immediate @term`.
 
-  **Variants:**
+   .. cmdv:: Hint Constructors @ident
+      :name: Hint Constructors
 
-    + :n:`Constructors {+ @ident}`
-      Adds each :n:`Constructors @ident`.
+      If :n:`@ident` is an inductive type, this command adds all its constructors as
+      hints of type ``Resolve``. Then, when the conclusion of current goal has the form
+      :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor.
 
-+ :n:`Unfold @qualid`
-  This adds the tactic :n:`unfold @qualid` to the hint list that will only be
-  used when the head constant of the goal is :n:`@ident`.
-  Its cost is 4.
+   .. exn:: @ident is not an inductive type
 
-  **Variants:**
+   .. cmdv:: Hint Constructors {+ @ident}
 
-    + :n:`Unfold {+ @ident}`
-      Adds each :n:`Unfold @ident`.
+      Adds each :n:`Hint Constructors @ident`.
 
-+ :n:`Transparent`, :n:`Opaque @qualid`
-  This adds a transparency hint to the database, making :n:`@qualid` a
-  transparent or opaque constant during resolution. This information is used
-  during unification of the goal with any lemma in the database and inside the
-  discrimination network to relax or constrain it in the case of discriminated
-  databases.
+   .. cmdv:: Hint Unfold @qualid
+      :name: Hint Unfold
 
-  **Variants:**
+      This adds the tactic :n:`unfold @qualid` to the hint list that will only be
+      used when the head constant of the goal is :n:`@ident`.
+      Its cost is 4.
 
-    + :n:`Transparent`, :n:`Opaque {+ @ident}`
-      Declares each :n:`@ident` as a transparent or opaque constant.
+   .. cmdv:: Hint Unfold {+ @ident}
 
-+ :n:`Extern @num {? @pattern} => tactic`
-  This hint type is to extend ``auto`` with tactics other than ``apply`` and
-  ``unfold``. For that, we must specify a cost, an optional :n:`@pattern` and a
-  :n:`tactic` to execute. Here is an example::
-
-    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. 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::
-     .. 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.
-
-+ :n:`Cut @regexp`
-
-  .. warning:: these hints currently only apply to typeclass
-               proof search and the ``typeclasses eauto`` tactic (:ref:`typeclasses-eauto`).
-
-  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 ``Print HintDb`` to verify the current cut expression:
-
-  .. productionlist:: `regexp`
-     e : ident      hint or instance identifier
-     :|_         any hint
-     :| e\|e′     disjunction
-     :| e e′      sequence
-     :| e *       Kleene star
-     :| emp       empty
-     :| 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`.
-
-+ :n:`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.
+      Adds each :n:`Hint Unfold @ident`.
 
-.. note::
- One can use an ``Extern`` hint with no pattern to do pattern-matching on
- hypotheses using ``match goal`` with inside the tactic.
+   .. cmdv:: Hint %( Transparent %| Opaque %) @qualid
+      :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
+      during unification of the goal with any lemma in the database and inside the
+      discrimination network to relax or constrain it in the case of discriminated
+      databases.
+
+    .. cmdv:: Hint %(Transparent | Opaque) {+ @ident}
+
+      Declares each :n:`@ident` as a transparent or opaque constant.
+
+    .. 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.
+
+       .. example::
+
+          .. coqtop:: in
+
+             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. 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::
+
+          .. 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.
+
+    .. cmdv:: Hint Cut @regexp
+
+       .. warning::
+
+          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:
+
+       .. productionlist:: `regexp`
+          e : ident      hint or instance identifier
+            :|_         any hint
+            :| e\|e′     disjunction
+            :| e e′      sequence
+            :| e *       Kleene star
+            :| emp       empty
+            :| 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.
 
 
 Hint databases defined in the Coq standard library
@@ -3587,7 +3660,7 @@ non-imported hints.
 Setting implicit automation tactics
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Proof with tactic
+.. cmd:: Proof with @tactic
 
    This command may be used to start a proof. It defines a default tactic
    to be used each time a tactic command ``tactic``:sub:`1` is ended by ``...``.
@@ -3601,11 +3674,11 @@ Setting implicit automation tactics
 
       Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
-   .. cmdv:: Proof using {+ @ident} with tactic
+   .. cmdv:: Proof using {+ @ident} with @tactic
 
       Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
-   .. cmd:: Declare Implicit Tactic tactic
+   .. cmd:: Declare Implicit Tactic @tactic
 
       This command declares a tactic to be used to solve implicit arguments
       that Coq does not know how to solve by unification. It is used every
@@ -3669,11 +3742,12 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
   an instantiation of `x` is necessary.
 
 .. tacv:: dtauto
+   :name: dtauto
 
-  While :tacn:`tauto` recognizes inductively defined connectives isomorphic to
-  the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``,
-  :tacn:`dtauto` recognizes also all inductive types with one constructors and
-  no indices, i.e. record-style connectives.
+   While :tacn:`tauto` recognizes inductively defined connectives isomorphic to
+   the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``,
+   :tacn:`dtauto` recognizes also all inductive types with one constructors and
+   no indices, i.e. record-style connectives.
 
 .. tacn:: intuition @tactic
    :name: intuition
@@ -3746,13 +3820,15 @@ first- order reasoning, written by Pierre Corbineau. It is not restricted to
 usual logical connectives but instead may reason about any first-order class
 inductive definition.
 
-The default tactic used by :tacn:`firstorder` when no rule applies is :g:`auto
-with \*`, it can be reset locally or globally using the :opt:`Firstorder Solver`
-option and printed using :cmd:`Print Firstorder Solver`.
+.. opt:: Firstorder Solver
+
+   The default tactic used by :tacn:`firstorder` when no rule applies is
+   :g:`auto with *`, it can be reset locally or globally using this option and
+   printed using :cmd:`Print Firstorder Solver`.
 
 .. tacv:: firstorder @tactic
 
-  Tries to solve the goal with :n:`@tactic` when no logical rule may apply.
+   Tries to solve the goal with :n:`@tactic` when no logical rule may apply.
 
 .. tacv:: firstorder using {+ @qualid}
 
@@ -3991,6 +4067,7 @@ symbol :g:`=`.
 
 .. tacv:: esimplify_eq @num
 .. tacv:: esimplify_eq @term {? with @bindings_list}
+   :name: esimplify_eq
 
    This works the same as ``simplify_eq`` but if the type of :n:`@term`, or the
    type of the hypothesis referred to by :n:`@num`, has uninstantiated
@@ -4002,7 +4079,7 @@ symbol :g:`=`.
    :n:`intro @ident; simplify_eq @ident`.
 
 .. tacn:: dependent rewrite -> @ident
-   :name: dependent rewrite ->
+   :name: dependent rewrite
 
    This tactic applies to any goal. If :n:`@ident` has type
    :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each
@@ -4270,7 +4347,7 @@ This tactics reverses the list of the focused goals.
    This tactic moves all goals under focus to a shelf. While on the
    shelf, goals will not be focused on. They can be solved by
    unification, or they can be called back into focus with the command
-   :tacn:`Unshelve`.
+   :cmd:`Unshelve`.
 
 .. tacv:: shelve_unifiable
 
@@ -4286,8 +4363,7 @@ This tactics reverses the list of the focused goals.
       all:shelve_unifiable.
       reflexivity.
 
-.. tacn:: Unshelve
-   :name: Unshelve
+.. cmd:: Unshelve
 
    This command moves all the goals on the shelf (see :tacn:`shelve`)
    from the shelf into focus, by appending them to the end of the current
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 6a20c0466..d0d7d74af 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -39,6 +39,7 @@ This is a synonym to ``Print`` :n:`@qualid` when :n:`@qualid`
 denotes a global constant.
 
 .. cmdv:: About @qualid.
+   :name: About
 
 This displays various information about the object
 denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive,
@@ -61,6 +62,7 @@ Variants:
 
 
 .. cmdv:: Inspect @num.
+   :name: Inspect
 
 This command displays the :n:`@num` last objects of the
 current environment, including sections and modules.
@@ -186,9 +188,17 @@ This command prints the current value of :n:`@option`.
 .. TODO : table is not a syntax entry
 
 .. cmd:: Add @table @value.
+   :name: Add `table` `value`
+
 .. cmd:: Remove @table @value.
+   :name: Remove `table` `value`
+
 .. cmd:: Test @table @value.
+   :name: Test `table` `value`
+
 .. cmd:: Test @table for @value.
+   :name: Test `table` for `value`
+
 .. cmd:: Print Table @table.
 
 These are  general commands for tables.
@@ -693,9 +703,9 @@ 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:: Compiled library ident.vo makes inconsistent assumptions over library qualid
+.. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid
 
-The command tried to load library file `ident.vo` that
+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
@@ -761,7 +771,7 @@ Error messages:
 
 .. exn:: File not found on loadpath : @string
 
-.. exn:: Loading of ML object file forbidden in a native |Coq|
+.. exn:: Loading of ML object file forbidden in a native Coq
 
 
 
@@ -1025,16 +1035,13 @@ to |Coq| with the command:
 
     go();;
 
+.. warning::
 
-
-Warnings:
-
-
-#. 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`).
+   #. 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`).
 
 
 
@@ -1089,7 +1096,7 @@ Controlling display
 
    This option controls the normal displaying.
 
-.. opt:: Warnings "@ident {* , @ident }"
+.. opt:: Warnings "{+, {? %( - %| + %) } @ident }"
 
    This option configures the display of warnings. It is experimental, and
    expects, between quotes, a comma-separated list of warning names or
@@ -1129,10 +1136,10 @@ Controlling display
 .. opt:: Printing Unfocused
 
    This option controls whether unfocused goals are displayed. Such goals are
-   created by focusing other goals with bullets (see :ref:`bullets`) or curly
-   braces (see `here <curly-braces>`). It is off by default.
+   created by focusing other goals with bullets (see :ref:`bullets` or
+   :ref:`curly braces <curly-braces>`). It is off by default.
 
-.. cmd:: Printing Dependent Evars Line
+.. opt:: Printing Dependent Evars Line
 
    This option controls the printing of the “(dependent evars: …)” line when
    ``-emacs`` is passed.
@@ -1150,7 +1157,7 @@ conversion algorithm lazily compares applicative terms while the other
 is a brute-force but efficient algorithm that first normalizes the
 terms before comparing them. The second algorithm is based on a
 bytecode representation of terms similar to the bytecode
-representation used in the ZINC virtual machine [`98`]. It is
+representation used in the ZINC virtual machine :cite:`Leroy90`. It is
 especially useful for intensive computation of algebraic values, such
 as numbers, and for reflection-based tactics. The commands to fine-
 tune the reduction strategies and the lazy conversion algorithm are