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

5 files changed, 1149 insertions, 1262 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 7ab11889f5..c5ee724caf 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -245,9 +245,10 @@ focused goals with:
    :name: ... : ... (goal selector)
 
    We can also use selectors as a tactical, which allows to use them nested
-   in a tactic expression, by using the keyword ``only``:
+   in a tactic expression, by using the keyword :tacn:`only`:
 
    .. tacv:: only selector : expr
+      :name: only ... : ...
 
       When selecting several goals, the tactic expr is applied globally to all
       selected goals.
@@ -268,6 +269,7 @@ focused goals with:
       for ``n-n`` when specifying multiple ranges.
 
    .. tacv:: all: @expr
+      :name: all: ...
 
       In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only
       be used at the toplevel of a tactic expression.
@@ -279,6 +281,7 @@ focused goals with:
       used at the toplevel of a tactic expression.
 
    .. tacv:: par: @expr
+      :name: par: ...
 
       In this variant, :n:`@expr` is applied to all focused goals in parallel.
       The number of workers can be controlled via the command line option
@@ -288,8 +291,8 @@ focused goals with:
       nothing (i.e. it cannot make some progress). ``par:`` can only be used at
       the toplevel of a tactic expression.
 
-   .. exn:: No such goal
-      :name: No such goal (goal selector)
+   .. exn:: No such goal.
+      :name: No such goal. (Goal selector)
 
    .. TODO change error message index entry
 
@@ -348,7 +351,7 @@ We can check if a tactic made progress with:
    to one of the focused subgoal produced subgoals equal to the initial
    goals (up to syntactical equality), then an error of level 0 is raised.
 
-   .. exn:: Failed to progress
+   .. exn:: Failed to progress.
 
 Backtracking branching
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -389,7 +392,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics:
    :n:`first [:@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first
    :n:`v__i` to have *at least* one success.
 
-   .. exn:: Error message: No applicable tactic
+   .. exn:: No applicable tactic.
 
    .. tacv:: first @expr
 
@@ -478,7 +481,7 @@ one* success:
       whether a second success exists, and may run further effects
       immediately.
 
-   .. exn:: This tactic has more than one success
+   .. exn:: This tactic has more than one success.
 
 Checking the failure
 ~~~~~~~~~~~~~~~~~~~~
@@ -516,7 +519,7 @@ among a panel of tactics:
    each goal independently, if it doesn’t solve the goal then it tries to
    apply :n:`v__2` and so on. It fails if there is no solving tactic.
 
-   .. exn:: Cannot solve the goal
+   .. exn:: Cannot solve the goal.
 
    .. tacv:: solve @expr
 
@@ -547,7 +550,7 @@ Failing
    :tacn:`fail` tactic will, however, succeed if all the goals have already been
    solved.
 
-   .. tacv:: fail @natural
+   .. tacv:: fail @num
 
       The number is the failure level. If no level is specified, it defaults to 0.
       The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
@@ -555,14 +558,14 @@ Failing
       (backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`,
       :tacn:`repeat`, or branching command is aborted and the level is decremented. In
       the case of :n:`+`, a non-zero level skips the first backtrack point, even if
-      the call to :n:`fail @natural` is not enclosed in a :n:`+` command,
+      the call to :n:`fail @num` is not enclosed in a :n:`+` command,
       respecting the algebraic identity.
 
    .. tacv:: fail {* message_token}
 
       The given tokens are used for printing the failure message.
 
-   .. tacv:: fail @natural {* message_token}
+   .. tacv:: fail @num {* message_token}
 
       This is a combination of the previous variants.
 
@@ -573,7 +576,7 @@ Failing
 
    .. tacv:: gfail {* message_token}
 
-   .. tacv:: gfail @natural {* message_token}
+   .. tacv:: gfail @num {* message_token}
 
       These variants fail with an error message or an error level even if
       there are no goals left. Be careful however if Coq terms have to be
@@ -581,7 +584,7 @@ Failing
       tactic into the goals, meaning that if there are no goals when it is
       evaluated, a tactic call like :n:`let x:=H in fail 0 x` will succeed.
 
-   .. exn:: Tactic Failure message (level @natural).
+   .. exn:: Tactic Failure message (level @num).
 
 Timeout
 ~~~~~~~
@@ -760,11 +763,11 @@ We can carry out pattern matching on terms with:
    branches or inside the right-hand side of the selected branch even if it
    has backtracking points.
 
-   .. exn:: No matching clauses for match
+   .. exn:: No matching clauses for match.
 
       No pattern can be used and, in particular, there is no :n:`_` pattern.
 
-   .. exn:: Argument of match does not evaluate to a term
+   .. exn:: Argument of match does not evaluate to a term.
 
       This happens when :n:`@expr` does not denote a term.
 
@@ -844,7 +847,7 @@ We can make pattern matching on goals using the following expression:
    branches or combinations of hypotheses, or inside the right-hand side of
    the selected branch even if it has backtracking points.
 
-   .. exn:: No matching clauses for match goal
+   .. exn:: No matching clauses for match goal.
 
       No clause succeeds, i.e. all matching patterns, if any, fail at the
       application of the right-hand-side.
@@ -891,7 +894,7 @@ produce subgoals but generates a term to be used in tactic expressions:
    match expression. This expression evaluates replaces the hole of the
    value of :n:`@ident` by the value of :n:`@expr`.
 
-   .. exn:: not a context variable
+   .. exn:: Not a context variable.
 
 Generating fresh hypothesis names
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1001,7 +1004,7 @@ Testing boolean expressions
          all:let n:= numgoals in guard n<4.
          Fail all:let n:= numgoals in guard n=2.
 
-   .. exn:: Condition not satisfied
+   .. exn:: Condition not satisfied.
 
 Proving a subgoal as a separate lemma
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1051,8 +1054,8 @@ Proving a subgoal as a separate lemma
          with tactics is fragile, and explicitly named and reused subterms
          don’t play well with asynchronous proofs.
 
-   .. exn:: Proof is not complete
-      :name: Proof is not complete (abstract)
+   .. exn:: Proof is not complete.
+      :name: Proof is not complete. (abstract)
 
 Tactic toplevel definitions
 ---------------------------
@@ -1092,7 +1095,7 @@ Basically, |Ltac| toplevel definitions are made as follows:
 Printing |Ltac| tactics
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Print Ltac @qualid.
+.. cmd:: Print Ltac @qualid
 
    Defined |Ltac| functions can be displayed using this command.
 
@@ -1107,10 +1110,11 @@ Info trace
 ~~~~~~~~~~
 
 .. cmd:: Info @num @expr
+   :name: Info
 
    This command can be used to print the trace of the path eventually taken by an
    |Ltac| script. That is, the list of executed tactics, discarding
-   all the branches which have failed. To that end the Info command can be
+   all the branches which have failed. To that end the :cmd:`Info` command can be
    used with the following syntax.
 
 
@@ -1137,23 +1141,22 @@ Info trace
 
          Info 1 t 1||t 0.
 
-   The trace produced by ``Info`` tries its best to be a reparsable
+   The trace produced by :cmd:`Info` tries its best to be a reparsable
    |Ltac| script, but this goal is not achievable in all generality.
    So some of the output traces will contain oddities.
 
-   As an additional help for debugging, the trace produced by ``Info`` contains
-   (in comments) the messages produced by the idtac
-   tacticals \ `4.2 <#ltac%3Aidtac>`__ at the right possition in the
-   script. In particular, the calls to idtac in branches which failed are
+   As an additional help for debugging, the trace produced by :cmd:`Info` contains
+   (in comments) the messages produced by the :tacn:`idtac` tactical at the right
+   position in the script. In particular, the calls to idtac in branches which failed are
    not printed.
 
-   .. opt:: Info Level @num.
+   .. opt:: Info Level @num
 
-      This option is an alternative to the ``Info`` command.
+      This option is an alternative to the :cmd:`Info` command.
 
       This will automatically print the same trace as :n:`Info @num` at each
       tactic call. The unfolding level can be overridden by a call to the
-      ``Info`` command.
+      :cmd:`Info` command.
 
 Interactive debugger
 ~~~~~~~~~~~~~~~~~~~~
@@ -1223,7 +1226,7 @@ performance bug.
 
    .. warning::
 
-      Backtracking across a Reset Ltac Profile will not restore the information.
+      Backtracking across a :cmd:`Reset Ltac Profile` will not restore the information.
 
 .. coqtop:: reset in
 
@@ -1286,8 +1289,8 @@ performance bug.
    benchmarking purposes.
 
 You can also pass the ``-profile-ltac`` command line option to ``coqc``, which
-performs a ``Set Ltac Profiling`` at the beginning of each document, and a
-``Show Ltac Profile`` at the end.
+turns the :opt:`Ltac Profiling` option on at the beginning of each document,
+and performs a :cmd:`Show Ltac Profile` at the end.
 
 .. warning::
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 86c94bab36..df8ef74f74 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -34,7 +34,7 @@ terms of λ-calculus, known as the *Curry-Howard isomorphism*
 terms are called *proof terms*.
 
 
-.. exn:: No focused proof
+.. exn:: No focused proof.
 
 Coq raises this error message when one attempts to use a proof editing command
 out of the proof editing mode.
@@ -49,7 +49,7 @@ the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
 list of assertion commands is given in Section :ref:`Assertions`. The command
 :cmd:`Goal` can also be used.
 
-.. cmd:: Goal @form.
+.. cmd:: Goal @form
 
 This is intended for quick assertion of statements, without knowing in
 advance which name to give to the assertion, typically for quick
@@ -68,7 +68,7 @@ proof term to the declared name of the original goal. This name is
 added to the environment as an opaque constant.
 
 
-.. exn:: Attempt to save an incomplete proof
+.. exn:: Attempt to save an incomplete proof.
 
 .. note::
 
@@ -81,34 +81,36 @@ proof term is completely rechecked at this point, one may have to wait
 a while when the proof is large. In some exceptional cases one may
 even incur a memory overflow.
 
-.. cmdv:: Defined.
+.. cmdv:: Defined
    :name: Defined (interactive proof)
 
 Defines the proved term as a transparent constant.
 
-.. cmdv:: Save @ident.
+.. cmdv:: Save @ident
 
 Forces the name of the original goal to be :n:`@ident`. This
 command (and the following ones) can only be used if the original goal
 has been opened using the ``Goal`` command.
 
-.. cmd:: Admitted.
+.. cmd:: Admitted
    :name: Admitted (interactive proof)
 
-This command is available in interactive editing proof mode to give up
+This command is available in interactive editing mode to give up
 the current proof and declare the initial goal as an axiom.
 
-.. cmd:: Proof @term.
+.. cmd:: Proof @term
    :name: Proof `term`
 
 This command applies in proof editing mode. It is equivalent to
 
-.. cmd:: exact @term. Qed.
+.. coqtop:: in
+
+   exact @term. Qed.
 
 That is, you have to give the full proof in one gulp, as a
 proof term (see Section :ref:`applyingtheorems`).
 
-.. cmdv:: Proof.
+.. cmdv:: Proof
    :name: Proof (interactive proof)
 
 Is a noop which is useful to delimit the sequence of tactic commands
@@ -121,7 +123,7 @@ See also: ``Proof with tactic.`` in Section
 :ref:`tactics-implicit-automation`.
 
 
-.. cmd:: Proof using @ident1 ... @identn.
+.. cmd:: Proof using @ident1 ... @identn
 
 This command applies in proof editing mode. It declares the set of
 section variables (see :ref:`gallina-assumptions`) used by the proof. At ``Qed`` time, the
@@ -133,23 +135,23 @@ example if ``T`` is variable and a is a variable of type ``T``, the commands
 ``Proof using a`` and ``Proof using T a``` are actually equivalent.
 
 
-.. cmdv:: Proof using @ident1 ... @identn with @tactic.
+.. cmdv:: Proof using @ident1 ... @identn with @tactic
 
 in Section :ref:`tactics-implicit-automation`.
 
-.. cmdv:: Proof using All.
+.. cmdv:: Proof using All
 
 Use all section variables.
 
 
-.. cmdv:: Proof using Type.
+.. cmdv:: Proof using Type
 
-.. cmdv:: Proof using.
+.. cmdv:: Proof using
 
 Use only section variables occurring in the statement.
 
 
-.. cmdv:: Proof using Type*.
+.. cmdv:: Proof using Type*
 
 The ``*`` operator computes the forward transitive closure. E.g. if the
 variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type
@@ -157,21 +159,21 @@ of ``H``. ``Type*`` is the forward transitive closure of the entire set of
 section variables occurring in the statement.
 
 
-.. cmdv:: Proof using -(@ident1 ... @identn).
+.. cmdv:: Proof using -(@ident1 ... @identn)
 
 Use all section variables except :n:`@ident1` ... :n:`@identn`.
 
 
-.. cmdv:: Proof using @collection1 + @collection2 .
+.. cmdv:: Proof using @collection1 + @collection2
 
 
-.. cmdv:: Proof using @collection1 - @collection2 .
+.. cmdv:: Proof using @collection1 - @collection2
 
 
-.. cmdv:: Proof using @collection - ( @ident1 ... @identn ).
+.. cmdv:: Proof using @collection - ( @ident1 ... @identn )
 
 
-.. cmdv:: Proof using @collection * .
+.. cmdv:: Proof using @collection *
 
 Use section variables being, respectively, in the set union, set
 difference, set complement, set forward transitive closure. See
@@ -185,14 +187,14 @@ Proof using options
 The following options modify the behavior of ``Proof using``.
 
 
-.. opt:: Default Proof Using "@expression".
+.. opt:: Default Proof Using "@expression"
 
    Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default
    Proof Using "a b"``. will complete all ``Proof`` commands not followed by a
    using part with using ``a`` ``b``.
 
 
-.. opt:: Suggest Proof Using.
+.. opt:: Suggest Proof Using
 
    When ``Qed`` is performed, suggest a using annotation if the user did not
    provide one.
@@ -232,29 +234,29 @@ Define the collection named "Many" containing the set difference of
 "Fewer" and the unnamed collection ``x`` ``y``
 
 
-.. cmd:: Abort.
+.. cmd:: Abort
 
 This command cancels the current proof development, switching back to
 the previous proof development, or to the |Coq| toplevel if no other
 proof was edited.
 
 
-.. exn:: No focused proof (No proof-editing in progress)
+.. exn:: No focused proof (No proof-editing in progress).
 
 
 
-.. cmdv::  Abort @ident.
+.. cmdv::  Abort @ident
 
 Aborts the editing of the proof named :n:`@ident`.
 
-.. cmdv:: Abort All.
+.. cmdv:: Abort All
 
 Aborts all current goals, switching back to the |Coq|
 toplevel.
 
 
 
-.. cmd:: Existential @num := @term.
+.. cmd:: Existential @num := @term
 
 This command instantiates an existential variable. :n:`@num` is an index in
 the list of uninstantiated existential variables displayed by ``Show
@@ -271,7 +273,7 @@ See also: ``instantiate (num:= term).`` in Section
 See also: ``Grab Existential Variables.`` below.
 
 
-.. cmd:: Grab Existential Variables.
+.. cmd:: Grab Existential Variables
 
 This command can be run when a proof has no more goal to be solved but
 has remaining uninstantiated existential variables. It takes every
@@ -281,84 +283,80 @@ uninstantiated existential variable and turns it into a goal.
 Navigation in the proof tree
 --------------------------------
 
+.. cmd:: Undo
 
-.. cmd:: Undo.
-
-This command cancels the effect of the last command. Thus, it
-backtracks one step.
-
+   This command cancels the effect of the last command. Thus, it
+   backtracks one step.
 
-.. cmdv:: Undo @num.
+.. cmdv:: Undo @num
 
-Repeats Undo :n:`@num` times.
+   Repeats Undo :n:`@num` times.
 
-.. cmdv:: Restart.
+.. cmdv:: Restart
    :name: Restart
 
-This command restores the proof editing process to the original goal.
+   This command restores the proof editing process to the original goal.
 
+   .. exn:: No focused proof to restart.
 
-.. exn:: No focused proof to restart
+.. cmd:: Focus
 
+   This focuses the attention on the first subgoal to prove and the
+   printing of the other subgoals is suspended until the focused subgoal
+   is solved or unfocused. This is useful when there are many current
+   subgoals which clutter your screen.
 
-.. cmd:: Focus.
+.. cmdv:: Focus @num
 
-This focuses the attention on the first subgoal to prove and the
-printing of the other subgoals is suspended until the focused subgoal
-is solved or unfocused. This is useful when there are many current
-subgoals which clutter your screen.
+   This focuses the attention on the :n:`@num` th subgoal to prove.
 
+   .. deprecated:: 8.8
 
-.. cmdv:: Focus @num.
+      Prefer the use of bullets or
+      focusing brackets instead, including :n:`@num : %{`
 
-This focuses the attention on the :n:`@num` th subgoal to
-prove.
+.. cmd:: Unfocus
 
-*This command is deprecated since 8.8*: prefer the use of bullets or
-focusing brackets instead, including :n:`@num : %{`
+   This command restores to focus the goal that were suspended by the
+   last ``Focus`` command.
 
-.. cmd:: Unfocus.
+   .. deprecated:: 8.8
 
-This command restores to focus the goal that were suspended by the
-last ``Focus`` command.
+.. cmd:: Unfocused
 
-*This command is deprecated since 8.8.*
-
-.. cmd:: Unfocused.
-
-Succeeds if the proof is fully unfocused, fails is there are some
-goals out of focus.
+   Succeeds if the proof is fully unfocused, fails if there are some
+   goals out of focus.
 
 .. _curly-braces:
 
 .. cmd:: %{ %| %}
 
-The command ``{`` (without a terminating period) focuses on the first
-goal, much like ``Focus.`` does, however, the subproof can only be
-unfocused when it has been fully solved ( *i.e.* when there is no
-focused goal left). Unfocusing is then handled by ``}`` (again, without a
-terminating period). See also example in next section.
+   The command ``{`` (without a terminating period) focuses on the first
+   goal, much like ``Focus.`` does, however, the subproof can only be
+   unfocused when it has been fully solved ( *i.e.* when there is no
+   focused goal left). Unfocusing is then handled by ``}`` (again, without a
+   terminating period). See also example in next section.
 
-Note that when a focused goal is proved a message is displayed
-together with a suggestion about the right bullet or ``}`` to unfocus it
-or focus the next one.
+   Note that when a focused goal is proved a message is displayed
+   together with a suggestion about the right bullet or ``}`` to unfocus it
+   or focus the next one.
 
 .. cmdv:: @num: %{
 
-This focuses on the :n:`@num` th subgoal to prove.
+   This focuses on the :n:`@num` th subgoal to prove.
 
-Error messages:
+   Error messages:
 
-.. exn:: This proof is focused, but cannot be unfocused this way
+   .. exn:: This proof is focused, but cannot be unfocused this way.
 
-You are trying to use ``}`` but the current subproof has not been fully solved.
+      You are trying to use ``}`` but the current subproof has not been fully solved.
 
-.. exn:: No such goal
-   :name: No such goal (focusing)
+   .. exn:: No such goal.
+      :name: No such goal. (Focusing)
 
-.. exn:: Brackets only support the single numbered goal selector
+   .. exn:: Brackets only support the single numbered goal selector.
 
-See also error messages about bullets below.
+      See also error messages about bullets below.
 
 .. _bullets:
 
@@ -409,11 +407,11 @@ The following example script illustrates all these features:
     assumption.
 
 
-.. exn:: Wrong bullet @bullet1 : Current bullet @bullet2 is not finished.
+.. exn:: Wrong bullet @bullet1: Current bullet @bullet2 is not finished.
 
 Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same.
 
-.. exn:: Wrong bullet @bullet1 : Bullet @bullet2 is mandatory here.
+.. exn:: Wrong bullet @bullet1: Bullet @bullet2 is mandatory here.
 
 You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here.
 
@@ -427,17 +425,12 @@ You just finished a goal focused by ``{``, you must unfocus it with ``}``.
 
 Set Bullet Behavior
 ```````````````````
+.. opt:: Bullet Behavior  %( "None" %| "Strict Subproofs" %)
 
-The bullet behavior can be controlled by the following commands.
-
-.. opt:: Bullet Behavior "None"
-
-This makes bullets inactive.
-
-.. opt:: Bullet Behavior "Strict Subproofs"
-
-This makes bullets active (this is the default behavior).
+   This option controls the bullet behavior and can take two possible values:
 
+   - "None": this makes bullets inactive.
+   - "Strict Subproofs": this makes bullets active (this is the default behavior).
 
 .. _requestinginformation:
 
@@ -445,7 +438,7 @@ Requesting information
 ----------------------
 
 
-.. cmd:: Show.
+.. cmd:: Show
 
 This command displays the current goals.
 
@@ -454,10 +447,10 @@ This command displays the current goals.
 
 Displays only the :n:`@num`-th subgoal.
 
-.. exn:: No such goal
-.. exn:: No focused proof
+.. exn:: No such goal.
+.. exn:: No focused proof.
 
-.. cmdv:: Show @ident.
+.. cmdv:: Show @ident
 
 Displays the named goal :n:`@ident`. This is useful in
 particular to display a shelved goal but only works if the
@@ -472,7 +465,7 @@ corresponding existential variable has been named by the user
     eexists ?[n].
     Show n.
 
-.. cmdv:: Show Script.
+.. cmdv:: Show Script
 
 Displays the whole list of tactics applied from the
 beginning of the current proof. This tactics script may contain some
@@ -480,7 +473,7 @@ holes (subgoals not yet proved). They are printed under the form
 
 ``<Your Tactic Text here>``.
 
-.. cmdv:: Show Proof.
+.. cmdv:: Show Proof
 
 It displays the proof term generated by the tactics
 that have been applied. If the proof is not completed, this term
@@ -490,14 +483,14 @@ integer, and applied to the list of variables in the context, since it
 may depend on them. The types obtained by abstracting away the context
 from the type of each hole-placer are also printed.
 
-.. cmdv:: Show Conjectures.
+.. cmdv:: Show Conjectures
 
 It prints the list of the names of all the
 theorems that are currently being proved. As it is possible to start
 proving a previous lemma during the proof of a theorem, this list may
 contain several names.
 
-.. cmdv:: Show Intro.
+.. cmdv:: Show Intro
 
 If the current goal begins by at least one product,
 this command prints the name of the first product, as it would be
@@ -507,18 +500,18 @@ Proof General macro, it is possible to transform any anonymous ``intro``
 into a qualified one such as ``intro y13``. In the case of a non-product
 goal, it prints nothing.
 
-.. cmdv:: Show Intros.
+.. cmdv:: Show Intros
 
 This command is similar to the previous one, it
 simulates the naming process of an intros.
 
-.. cmdv:: Show Existentials.
+.. cmdv:: Show Existentials
 
 It displays the set of all uninstantiated
 existential variables in the current proof tree, along with the type
 and the context of each variable.
 
-.. cmdv:: Show Match @ident.
+.. cmdv:: Show Match @ident
 
 This variant displays a template of the Gallina
 ``match`` construct with a branch for each constructor of the type
@@ -529,26 +522,26 @@ This variant displays a template of the Gallina
 
      Show Match nat.
 
-.. exn:: Unknown inductive type
+.. exn:: Unknown inductive type.
 
 .. _ShowUniverses:
 
-.. cmdv:: Show Universes.
+.. cmdv:: Show Universes
 
 It displays the set of all universe constraints and
 its normalized form at the current stage of the proof, useful for
 debugging universe inconsistencies.
 
 
-.. cmd:: Guarded.
+.. cmd:: Guarded
 
-Some tactics (e.g. :tacn:`refine` :ref:`applyingtheorems`) allow to build proofs using
+Some tactics (e.g. :tacn:`refine`) allow to build proofs using
 fixpoint or co-fixpoint constructions. Due to the incremental nature
 of interactive proof construction, the check of the termination (or
 guardedness) of the recursive calls in the fixpoint or cofixpoint
 constructions is postponed to the time of the completion of the proof.
 
-The command ``Guarded`` allows checking if the guard condition for
+The command :cmd:`Guarded` allows checking if the guard condition for
 fixpoint and cofixpoint is violated at some time of the construction
 of the proof without having to wait the completion of the proof.
 
@@ -570,13 +563,12 @@ available hypotheses.
 
 This option controls the way binders are handled
 in assertion commands such as ``Theorem ident [binders] : form``. When the
-option is set, which is the default, binders are automatically put in
+option is on, which is the default, binders are automatically put in
 the local context of the goal to prove.
 
-The option can be unset by issuing ``Unset Automatic Introduction``. When
-the option is unset, binders are discharged on the statement to be
-proved and a tactic such as intro (see Section :ref:`managingthelocalcontext`) has to be
-used to move the assumptions to the local context.
+When the option is off, binders are discharged on the statement to be
+proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
+has to be used to move the assumptions to the local context.
 
 
 Controlling memory usage
@@ -586,15 +578,15 @@ When experiencing high memory usage the following commands can be used
 to force |Coq| to optimize some of its internal data structures.
 
 
-.. cmd:: Optimize Proof.
+.. cmd:: Optimize Proof
 
 This command forces |Coq| to shrink the data structure used to represent
 the ongoing proof.
 
 
-.. cmd:: Optimize Heap.
+.. cmd:: Optimize Heap
 
 This command forces the |OCaml| runtime to perform a heap compaction.
 This is in general an expensive operation.
 See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-There is also an analogous tactic :tac:`optimize_heap`.
+There is also an analogous tactic :tacn:`optimize_heap`.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 977a5b8fad..63cd0f3ead 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -423,7 +423,7 @@ an improvement over ``all null s``.
 
 The syntax of the new declaration is
 
-.. cmd:: Prenex Implicits {+ @ident}.
+.. cmd:: Prenex Implicits {+ @ident}
 
 Let us denote :math:`c_1` … :math:`c_n` the list of identifiers given to a
 ``Prenex Implicits`` command.  The command checks that each ci is the name of
@@ -2157,10 +2157,10 @@ equivalent to:
 
 More generally, the tactic:
 
-.. tacn:: @tactic; last @natural first
+.. tacn:: @tactic; last @num first
    :name: last first
 
-where :token:`natural` is a |Coq| numeral, or and Ltac variable
+where :token:`num` is a |Coq| numeral, or an Ltac variable
 denoting a |Coq|
 numeral, having the value k. It rotates the n subgoals G1 , …, Gn
 generated by tactic. The first subgoal becomes Gn + 1 − k and the
@@ -2168,7 +2168,7 @@ circular order of subgoals remains unchanged.
 
 Conversely, the tactic:
 
-.. tacn:: @tactic; first @natural last
+.. tacn:: @tactic; first @num last
    :name: first last
 
 rotates the n subgoals G1 , …, Gn generated by tactic in order that
@@ -5322,11 +5322,11 @@ intro item  see :ref:`introduction_ssr`
 
 multiplier  see :ref:`iteration_ssr`
 
-.. prodn:: occ_switch ::= { {? + %| - } {* @natural } }
+.. prodn:: occ_switch ::= { {? + %| - } {* @num } }
 
 occur. switch see :ref:`occurrence_selection_ssr`
 
-.. prodn:: mult ::= {? @natural } @mult_mark
+.. prodn:: mult ::= {? @num } @mult_mark
 
 multiplier see :ref:`iteration_ssr`
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6c1b1c08c1..b3537bad80 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -92,7 +92,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
   the ``n``-th non dependent premise of the ``term``, as determined by the type
   of ``term``.
 
-  .. exn:: No such binder
+  .. exn:: No such binder.
 
 + A bindings list can also be a simple list of terms :n:`{* term}`.
   In that case the references to which these terms correspond are
@@ -151,8 +151,8 @@ no numbers are given, all occurrences of :n:`@term` in the goal are selected.
 Finally, the last notation is an abbreviation for ``* |- *``. Note also
 that ``|-`` is optional in the first case when no ``*`` is given.
 
-Here are some tactics that understand occurrences clauses: ``set``, ``remember``
-, ``induction``, ``destruct``.
+Here are some tactics that understand occurrences clauses: :tacn:`set`, :tacn:`remember`
+, :tacn:`induction`, :tacn:`destruct`.
 
 
 See also: :ref:`Managingthelocalcontext`,
@@ -167,201 +167,203 @@ Applying theorems
 .. tacn:: exact @term
    :name: exact
 
-This tactic applies to any goal. It gives directly the exact proof
-term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then
-``exact p`` succeeds iff ``T`` and ``U`` are convertible (see
-:ref:`Conversion-rules`).
+   This tactic applies to any goal. It gives directly the exact proof
+   term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then
+   ``exact p`` succeeds iff ``T`` and ``U`` are convertible (see
+   :ref:`Conversion-rules`).
 
-.. exn:: Not an exact proof.
+   .. exn:: Not an exact proof.
 
-.. tacv:: eexact @term.
-   :name: eexact
+   .. tacv:: eexact @term.
+      :name: eexact
 
-This tactic behaves like exact but is able to handle terms and goals with
-meta-variables.
+      This tactic behaves like exact but is able to handle terms and goals with
+      meta-variables.
 
 .. tacn:: assumption
    :name: assumption
 
-This tactic looks in the local context for an hypothesis which type is equal to
-the goal. If it is the case, the subgoal is proved. Otherwise, it fails.
+   This tactic looks in the local context for an hypothesis which type is equal to
+   the goal. If it is the case, the subgoal is proved. Otherwise, it fails.
 
-.. exn:: No such assumption.
+   .. exn:: No such assumption.
 
-.. tacv:: eassumption
-   :name: eassumption
+   .. tacv:: eassumption
+      :name: eassumption
 
-This tactic behaves like assumption but is able to handle goals with
-meta-variables.
+      This tactic behaves like assumption but is able to handle goals with
+      meta-variables.
 
 .. tacn:: refine @term
    :name: refine
 
-This tactic applies to any goal. It behaves like exact with a big
-difference: the user can leave some holes (denoted by ``_`` or``(_:type)``) in
-the term. refine will generate as many subgoals as there are holes in
-the term. The type of holes must be either synthesized by the system
-or declared by an explicit cast like ``(_:nat->Prop)``. Any subgoal that
-occurs in other subgoals is automatically shelved, as if calling
-shelve_unifiable (see Section 8.17.4). This low-level tactic can be
-useful to advanced users.
+   This tactic applies to any goal. It behaves like :tacn:`exact` with a big
+   difference: the user can leave some holes (denoted by ``_`` or ``(_:type)``) in
+   the term. :tacn:`refine` will generate as many subgoals as there are holes in
+   the term. The type of holes must be either synthesized by the system
+   or declared by an explicit cast like ``(_:nat->Prop)``. Any subgoal that
+   occurs in other subgoals is automatically shelved, as if calling
+   :tacn:`shelve_unifiable`. This low-level tactic can be
+   useful to advanced users.
 
-.. example::
-  .. coqtop:: reset all
+   .. example::
+      .. coqtop:: reset all
 
-     Inductive Option : Set :=
-     | Fail : Option
-     | Ok : bool -> Option.
+         Inductive Option : Set :=
+         | Fail : Option
+         | Ok : bool -> Option.
 
-     Definition get : forall x:Option, x <> Fail -> bool.
+         Definition get : forall x:Option, x <> Fail -> bool.
 
-     refine
-       (fun x:Option =>
-          match x return x <> Fail -> bool with
-          | Fail => _
-          | Ok b => fun _ => b
-          end).
+         refine
+           (fun x:Option =>
+           match x return x <> Fail -> bool with
+           | Fail => _
+           | Ok b => fun _ => b
+           end).
 
-     intros; absurd (Fail = Fail); trivial.
+         intros; absurd (Fail = Fail); trivial.
 
-     Defined.
+         Defined.
 
-.. exn:: invalid argument
+   .. exn:: Invalid argument.
 
-   The tactic ``refine`` does not know what to do with the term you gave.
+      The tactic :tacn:`refine` does not know what to do with the term you gave.
 
-.. exn:: Refine passed ill-formed term
+   .. exn:: Refine passed ill-formed term.
 
-   The term you gave is not a valid proof (not easy to debug in general). This
-   message may also occur in higher-level tactics that call ``refine``
-   internally.
+      The term you gave is not a valid proof (not easy to debug in general). This
+      message may also occur in higher-level tactics that call :tacn:`refine`
+      internally.
 
-.. exn:: Cannot infer a term for this placeholder
+   .. exn:: Cannot infer a term for this placeholder.
+      :name: Cannot infer a term for this placeholder. (refine)
 
-   There is a hole in the term you gave which type cannot be inferred. Put a
-   cast around it.
+      There is a hole in the term you gave whose type cannot be inferred. Put a
+      cast around it.
 
-.. tacv:: simple refine @term
-   :name: simple refine
+   .. tacv:: simple refine @term
+      :name: simple refine
 
-   This tactic behaves like refine, but it does not shelve any subgoal. It does
-   not perform any beta-reduction either.
+      This tactic behaves like refine, but it does not shelve any subgoal. It does
+      not perform any beta-reduction either.
 
-.. tacv:: notypeclasses refine @term
+   .. tacv:: notypeclasses refine @term
+      :name: notypeclasses refine
 
-   This tactic behaves like ``refine`` except it performs typechecking without
-   resolution of typeclasses.
+      This tactic behaves like :tacn:`refine` except it performs typechecking without
+      resolution of typeclasses.
 
-.. tacv:: simple notypeclasses refine @term
-   :name: simple notypeclasses refine
+   .. tacv:: simple notypeclasses refine @term
+      :name: simple notypeclasses refine
 
-   This tactic behaves like ``simple refine`` except it performs typechecking
-   without resolution of typeclasses.
+      This tactic behaves like :tacn:`simple refine` except it performs typechecking
+      without resolution of typeclasses.
 
-.. tacv:: apply @term
+.. tacn:: apply @term
    :name: apply
 
-This tactic applies to any goal. The argument term is a term well-formed in the
-local context. The tactic apply tries to match the current goal against the
-conclusion of the type of term. If it succeeds, then the tactic returns as many
-subgoals as the number of non-dependent premises of the type of term. If the
-conclusion of the type of term does not match the goal *and* the conclusion is
-an inductive type isomorphic to a tuple type, then each component of the tuple
-is recursively matched to the goal in the left-to-right order.
+   This tactic applies to any goal. The argument term is a term well-formed in the
+   local context. The tactic apply tries to match the current goal against the
+   conclusion of the type of term. If it succeeds, then the tactic returns as many
+   subgoals as the number of non-dependent premises of the type of term. If the
+   conclusion of the type of term does not match the goal *and* the conclusion is
+   an inductive type isomorphic to a tuple type, then each component of the tuple
+   is recursively matched to the goal in the left-to-right order.
 
-The tactic ``apply`` relies on first-order unification with dependent types
-unless the conclusion of the type of ``term`` is of the form :g:`P (t`:sub:`1`
-:g:`...` :g:`t`:sub:`n` :g:`)` with `P` to be instantiated. In the latter case, the behavior
-depends on the form of the goal. If the goal is of the form
-:g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n` and the :g:`t`:sub:`i` and
-:g:`u`:sub:`i` unifies, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise,
-``apply`` tries to define :g:`P` by abstracting over :g:`t`:sub:`1`  :g:`...`
-:g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it
-gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...`  :g:`u`:sub:`n`.
+   The tactic :tacn:`apply` relies on first-order unification with dependent types
+   unless the conclusion of the type of :token:`term` is of the form :g:`P (t`:sub:`1`
+   :g:`...` :g:`t`:sub:`n` :g:`)` with `P` to be instantiated. In the latter case, the behavior
+   depends on the form of the goal. If the goal is of the form
+   :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n` and the :g:`t`:sub:`i` and
+   :g:`u`:sub:`i` unifies, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise,
+   :tacn:`apply` tries to define :g:`P` by abstracting over :g:`t`:sub:`1`  :g:`...`
+   :g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it
+   gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...`  :g:`u`:sub:`n`.
 
-.. exn:: Unable to unify ... with ... .
+   .. exn:: Unable to unify ... with ... .
 
-The apply tactic failed to match the conclusion of term and the current goal.
-You can help the apply tactic by transforming your goal with the
-:tacn:`change` or :tacn:`pattern` tactics.
+      The apply tactic failed to match the conclusion of :token:`term` and the
+      current goal. You can help the apply tactic by transforming your goal with
+      the :tacn:`change` or :tacn:`pattern` tactics.
 
-.. exn:: Unable to find an instance for the variables {+ @ident}.
+   .. exn:: Unable to find an instance for the variables {+ @ident}.
 
-This occurs when some instantiations of the premises of term are not deducible
-from the unification. This is the case, for instance, when you want to apply a
-transitivity property. In this case, you have to use one of the variants below:
+      This occurs when some instantiations of the premises of :token:`term` are not deducible
+      from the unification. This is the case, for instance, when you want to apply a
+      transitivity property. In this case, you have to use one of the variants below:
 
-.. tacv:: apply @term with {+ @term}
+   .. tacv:: apply @term with {+ @term}
 
-Provides apply with explicit instantiations for all dependent premises of the
-type of term that do not occur in the conclusion and consequently cannot be
-found by unification. Notice that the collection :n:`{+ @term}` must be given
-according to the order of these dependent premises of the type of term.
+      Provides apply with explicit instantiations for all dependent premises of the
+      type of term that do not occur in the conclusion and consequently cannot be
+      found by unification. Notice that the collection :n:`{+ @term}` must be given
+      according to the order of these dependent premises of the type of term.
 
-.. exn:: Not the right number of missing arguments.
+      .. exn:: Not the right number of missing arguments.
 
-.. tacv:: apply @term with @bindings_list
+   .. tacv:: apply @term with @bindings_list
 
-This also provides apply with values for instantiating premises. Here, variables
-are referred by names and non-dependent products by increasing numbers (see
-:ref:`bindings list <bindingslist>`).
+      This also provides apply with values for instantiating premises. Here, variables
+      are referred by names and non-dependent products by increasing numbers (see
+      :ref:`bindings list <bindingslist>`).
 
-.. tacv:: apply {+, @term}
+   .. tacv:: apply {+, @term}
 
-This is a shortcut for ``apply term``:sub:`1`
-``; [.. | ... ; [ .. | apply`` ``term``:sub:`n` ``] ... ]``,
-i.e. for the successive applications of ``term``:sub:`i+1` on the last subgoal
-generated by ``apply term``:sub:`i` , starting from the application of
-``term``:sub:`1`.
+      This is a shortcut for :n:`apply @term`:sub:`1`
+      :n:`; [.. | ... ; [ .. | apply @term`:sub:`n` :n:`] ... ]`,
+      i.e. for the successive applications of :token:`term`:sub:`i+1` on the last subgoal
+      generated by :n:`apply @term`:sub:`i` , starting from the application of
+      :token:`term`:sub:`1`.
 
-.. tacv:: eapply @term
-   :name: eapply
+   .. tacv:: eapply @term
+      :name: eapply
 
-The tactic ``eapply`` behaves like ``apply`` but it does not fail when no
-instantiations are deducible for some variables in the premises. Rather, it
-turns these variables into existential variables which are variables still to
-instantiate (see :ref:`Existential-Variables`). The instantiation is
-intended to be found later in the proof.
+      The tactic :tacn:`eapply` behaves like :tacn:`apply` but it does not fail when no
+      instantiations are deducible for some variables in the premises. Rather, it
+      turns these variables into existential variables which are variables still to
+      instantiate (see :ref:`Existential-Variables`). The instantiation is
+      intended to be found later in the proof.
 
-.. tacv:: simple apply @term.
-   :name: simple apply
+   .. tacv:: simple apply @term.
+      :name: simple apply
 
-This behaves like ``apply`` but it reasons modulo conversion only on subterms
-that contain no variables to instantiate. For instance, the following example
-does not succeed because it would require the conversion of ``id ?foo`` and
-``O``.
+      This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms
+      that contain no variables to instantiate. For instance, the following example
+      does not succeed because it would require the conversion of ``id ?foo`` and
+      :g:`O`.
 
-.. example::
+      .. example::
 
-   .. coqtop:: all
+         .. coqtop:: all
 
-      Definition id (x : nat) := x.
-      Hypothesis H : forall y, id y = y.
-      Goal O = O.
-      Fail simple apply H.
+            Definition id (x : nat) := x.
+            Parameter H : forall y, id y = y.
+            Goal O = O.
+            Fail simple apply H.
 
-Because it reasons modulo a limited amount of conversion, ``simple apply`` fails
-quicker than ``apply`` and it is then well-suited for uses in user-defined
-tactics that backtrack often. Moreover, it does not traverse tuples as ``apply``
-does.
+      Because it reasons modulo a limited amount of conversion, :tacn:`simple apply` fails
+      quicker than :tacn:`apply` and it is then well-suited for uses in user-defined
+      tactics that backtrack often. Moreover, it does not traverse tuples as :tacn:`apply`
+      does.
 
-.. tacv:: {? simple} apply {+, @term {? with @bindings_list}}
-.. tacv:: {? simple} eapply {+, @term {? with @bindings_list}}
-   :name: simple eapply
+   .. tacv:: {? simple} apply {+, @term {? with @bindings_list}}
+   .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}}
+      :name: simple eapply
 
-This summarizes the different syntaxes for ``apply`` and ``eapply``.
+      This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`.
 
-.. tacv:: lapply @term
-   :name: lapply
+   .. tacv:: lapply @term
+      :name: lapply
 
-This tactic applies to any goal, say :g:`G`. The argument term has to be
-well-formed in the current context, its type being reducible to a non-dependent
-product :g:`A -> B` with :g:`B` possibly containing products. Then it generates
-two subgoals :g:`B->G` and :g:`A`. Applying ``lapply H`` (where :g:`H` has type
-:g:`A->B` and :g:`B` does not start with a product) does the same as giving the
-sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
+      This tactic applies to any goal, say :g:`G`. The argument term has to be
+      well-formed in the current context, its type being reducible to a non-dependent
+      product :g:`A -> B` with :g:`B` possibly containing products. Then it generates
+      two subgoals :g:`B->G` and :g:`A`. Applying ``lapply H`` (where :g:`H` has type
+      :g:`A->B` and :g:`B` does not start with a product) does the same as giving the
+      sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
 
-.. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product.
+      .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product.
 
 .. example::
    Assume we have a transitive relation ``R`` on ``nat``:
@@ -528,8 +530,8 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    constructor of :g:`I`, then ``constructor i`` is equivalent to
    ``intros; apply c``:sub:`i`.
 
-.. exn:: Not an inductive product
-.. exn:: Not enough constructors
+.. exn:: Not an inductive product.
+.. exn:: Not enough constructors.
 
 .. tacv:: constructor
 
@@ -562,7 +564,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    to :n:`intros; constructor 1 with @bindings_list.` It is typically used in
    the case of an existential quantification :math:`\exists`:g:`x, P(x).`
 
-.. exn:: Not an inductive goal with 1 constructor
+.. exn:: Not an inductive goal with 1 constructor.
 
 .. tacv:: exists @bindings_list
 
@@ -579,7 +581,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    Then, they are respectively equivalent to ``constructor 1`` and
    ``constructor 2``.
 
-.. exn:: Not an inductive goal with 2 constructors
+.. exn:: Not an inductive goal with 2 constructors.
 
 .. tacv:: left with @bindings_list
 .. tacv:: right with @bindings_list
@@ -656,7 +658,7 @@ be applied or the goal is not head-reducible.
    This applies ``intro`` but forces :n:`@ident` to be the name of the
    introduced hypothesis.
 
-.. exn:: name @ident is already used
+.. exn:: Name @ident is already used.
 
 .. note:: If a name used by intro hides the base name of a global
    constant then the latter can still be referred to by a qualified name
@@ -675,7 +677,7 @@ be applied or the goal is not head-reducible.
    `(@ident:term)` and discharges the variable named `ident` of the current
    goal.
 
-.. exn:: No such hypothesis in current goal
+.. exn:: No such hypothesis in current goal.
 
 .. tacv:: intros until @num
 
@@ -704,7 +706,7 @@ be applied or the goal is not head-reducible.
    too so as to respect the order of dependencies between hypotheses.
    Note that :n:`intro at bottom` is a synonym for :n:`intro` with no argument.
 
-.. exn:: No such hypothesis : @ident.
+.. exn:: No such hypothesis: @ident.
 
 .. tacv:: intro @ident after @ident
 .. tacv:: intro @ident before @ident
@@ -883,7 +885,7 @@ quantification or an implication.
    This tactic expects :n:`@ident` to be a local definition then clears its
    body. Otherwise said, this tactic turns a definition into an assumption.
 
-.. exn:: @ident is not a local definition
+.. exn:: @ident is not a local definition.
 
 .. tacv:: clear - {+ @ident}
 
@@ -950,9 +952,9 @@ the inverse of :tacn:`intro`.
    This moves ident at the bottom of the local context (at the end of the
    context).
 
-.. exn:: No such hypothesis
-.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident
-.. exn:: Cannot move @ident after @ident : it depends on @ident
+.. exn:: No such hypothesis.
+.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident.
+.. exn:: Cannot move @ident after @ident : it depends on @ident.
 
 .. example::
    .. coqtop:: all
@@ -979,8 +981,8 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    particular, the target identifiers may contain identifiers that exist in the
    source context, as long as the latter are also renamed by the same tactic.
 
-.. exn:: No such hypothesis
-.. exn:: @ident is already used
+.. exn:: No such hypothesis.
+.. exn:: @ident is already used.
 
 .. tacn:: set (@ident := @term)
    :name: set
@@ -992,7 +994,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    first checks that all subterms matching the pattern are compatible before
    doing the replacement using the leftmost subterm matching the pattern.
 
-.. exn:: The variable @ident is already defined
+.. exn:: The variable @ident is already defined.
 
 .. tacv:: set (@ident := @term ) in @goal_occurrences
 
@@ -1110,7 +1112,7 @@ Controlling the proof flow
    :g:`U` [2]_. The subgoal :g:`U` comes first in the list of subgoals remaining to
    prove.
 
-.. exn:: Not a proposition or a type
+.. exn:: Not a proposition or a type.
 
    Arises when the argument form is neither of type :g:`Prop`, :g:`Set` nor
    :g:`Type`.
@@ -1125,8 +1127,8 @@ Controlling the proof flow
    This tactic behaves like :n:`assert` but applies tactic to solve the subgoals
    generated by assert.
 
-   .. exn:: Proof is not complete
-      :name: Proof is not complete (assert)
+   .. exn:: Proof is not complete.
+      :name: Proof is not complete. (assert)
 
 .. tacv:: assert form as intro_pattern
 
@@ -1147,7 +1149,7 @@ Controlling the proof flow
    the type of :g:`term`. This is deprecated in favor of :n:`pose proof`. If the
    head of term is :n:`@ident`, the tactic behaves as :n:`specialize @term`.
 
-   .. exn:: Variable @ident is already declared
+   .. exn:: Variable @ident is already declared.
 
 .. tacv:: eassert form as intro_pattern by tactic
    :name: eassert
@@ -1239,8 +1241,8 @@ Controlling the proof flow
    the goal. The :n:`as` clause is especially useful in this case to immediately
    introduce the instantiated statement as a local hypothesis.
 
-   .. exn:: @ident is used in hypothesis @ident
-   .. exn:: @ident is used in conclusion
+   .. exn:: @ident is used in hypothesis @ident.
+   .. exn:: @ident is used in conclusion.
 
 .. tacn:: generalize @term
    :name: generalize
@@ -1364,7 +1366,7 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`.
    a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory
    hypotheses.
 
-.. exn:: No such assumption
+.. exn:: No such assumption.
 
 .. tacv:: contradiction @ident
 
@@ -1570,9 +1572,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       intros n H.
       induction n.
 
-.. exn:: Not an inductive product
+.. exn:: Not an inductive product.
 
-.. exn:: Unable to find an instance for the variables @ident ... @ident
+.. exn:: Unable to find an instance for the variables @ident ... @ident.
 
    Use in this case the variant :tacn:`elim ... with` below.
 
@@ -1846,8 +1848,8 @@ See also: :ref:`advanced-recursive-functions`
   :ref:`functional-scheme`
   :tacn:`inversion`
 
-.. exn:: Cannot find induction information on @qualid
-.. exn:: Not the right number of induction arguments
+.. exn:: Cannot find induction information on @qualid.
+.. exn:: Not the right number of induction arguments.
 
 .. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list
 
@@ -1880,8 +1882,8 @@ See also: :ref:`advanced-recursive-functions`
    :n:`@ident` is first introduced in the local context using
    :n:`intros until @ident`.
 
-.. exn:: No primitive equality found
-.. exn:: Not a discriminable equality
+.. exn:: No primitive equality found.
+.. exn:: Not a discriminable equality.
 
 .. tacv:: discriminate @num
 
@@ -1909,7 +1911,7 @@ See also: :ref:`advanced-recursive-functions`
    the form :n:`@term <> @term`, this behaves as
    :n:`intro @ident; discriminate @ident`.
 
-   .. exn:: No discriminable equalities
+   .. exn:: No discriminable equalities.
 
 .. tacn:: injection @term
    :name: injection
@@ -1920,7 +1922,7 @@ See also: :ref:`advanced-recursive-functions`
    :g:`t`:sub:`1` and :g:`t`:sub:`2` are equal too.
 
    If :n:`@term` is a proof of a statement of conclusion :n:`@term = @term`,
-   then ``injection`` applies the injectivity of constructors as deep as
+   then :tacn:`injection` applies the injectivity of constructors as deep as
    possible to derive the equality of all the subterms of :n:`@term` and
    :n:`@term` at positions where the terms start to differ. For example, from
    :g:`(S p, S n) = (q, S (S m))` we may derive :g:`S p = q` and
@@ -1930,93 +1932,96 @@ See also: :ref:`advanced-recursive-functions`
    equality of all the subterms at positions where they differ and adds them as
    antecedents to the conclusion of the current goal.
 
-.. example::
+   .. example::
 
-   Consider the following goal:
+      Consider the following goal:
 
-   .. coqtop:: reset all
+      .. coqtop:: in
 
-      Inductive list : Set :=
-      | nil : list
-      | cons : nat -> list -> list.
-      Variable P : list -> Prop.
-      Goal forall l n, P nil -> cons n l = cons 0 nil -> P l.
-      intros.
-      injection H0.
+         Inductive list : Set :=
+         | nil : list
+         | cons : nat -> list -> list.
+         Parameter P : list -> Prop.
+         Goal forall l n, P nil -> cons n l = cons 0 nil -> P l.
 
+      .. coqtop:: all
 
-Beware that injection yields an equality in a sigma type whenever the
-injected object has a dependent type :g:`P` with its two instances in
-different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and
-:g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and
-:g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable
-equality has been declared using the command ``Scheme Equality`` (see :ref:`proofschemes-induction-principles`),
-the use of a sigma type is avoided.
+         intros.
+         injection H0.
 
-.. note::
-   If some quantified hypothesis of the goal is named :n:`@ident`,
-   then :n:`injection @ident` first introduces the hypothesis in the local
-   context using :n:`intros until @ident`.
+   Beware that injection yields an equality in a sigma type whenever the
+   injected object has a dependent type :g:`P` with its two instances in
+   different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and
+   :g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and
+   :g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable
+   equality has been declared using the command :cmd:`Scheme Equality`
+   (see :ref:`proofschemes-induction-principles`),
+   the use of a sigma type is avoided.
 
-.. exn:: Not a projectable equality but a discriminable one
-.. exn:: Nothing to do, it is an equality between convertible @terms
-.. exn:: Not a primitive equality
-.. exn:: Nothing to inject
+   .. note::
+      If some quantified hypothesis of the goal is named :n:`@ident`,
+      then :n:`injection @ident` first introduces the hypothesis in the local
+      context using :n:`intros until @ident`.
 
-.. tacv:: injection @num
+   .. exn:: Not a projectable equality but a discriminable one.
+   .. exn:: Nothing to do, it is an equality between convertible @terms.
+   .. exn:: Not a primitive equality.
+   .. exn:: Nothing to inject.
 
-   This does the same thing as :n:`intros until @num` followed by
-   :n:`injection @ident` where :n:`@ident` is the identifier for the last
-   introduced hypothesis.
+   .. tacv:: injection @num
 
-.. tacv:: injection @term with @bindings_list
+      This does the same thing as :n:`intros until @num` followed by
+      :n:`injection @ident` where :n:`@ident` is the identifier for the last
+      introduced hypothesis.
 
-   This does the same as :n:`injection @term` but using the given bindings to
-   instantiate parameters or hypotheses of :n:`@term`.
+   .. tacv:: injection @term with @bindings_list
 
-.. tacv:: einjection @num
-.. tacv:: einjection @term {? with @bindings_list}
-   :name: einjection
+      This does the same as :n:`injection @term` but using the given bindings to
+      instantiate parameters or hypotheses of :n:`@term`.
 
-   This works the same as :n:`injection` but if the type of :n:`@term`, or the
-   type of the hypothesis referred to by :n:`@num`, has uninstantiated
-   parameters, these parameters are left as existential variables.
+   .. tacv:: einjection @num
+      :name: einjection
+   .. tacv:: einjection @term {? with @bindings_list}
+
+      This works the same as :n:`injection` but if the type of :n:`@term`, or the
+      type of the hypothesis referred to by :n:`@num`, has uninstantiated
+      parameters, these parameters are left as existential variables.
 
-.. tacv:: injection
+   .. tacv:: injection
 
-   If the current goal is of the form :n:`@term <> @term` , this behaves as
-   :n:`intro @ident; injection @ident`.
+      If the current goal is of the form :n:`@term <> @term` , this behaves as
+      :n:`intro @ident; injection @ident`.
 
-   .. exn:: goal does not satisfy the expected preconditions
+      .. exn:: goal does not satisfy the expected preconditions.
 
-.. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern}
-.. tacv:: injection @num as {+ intro_pattern}
-.. tacv:: injection as {+ intro_pattern}
-.. tacv:: einjection @term {? with @bindings_list} as {+ intro_pattern}
-.. tacv:: einjection @num as {+ intro_pattern}
-.. tacv:: einjection as {+ intro_pattern}
+   .. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern}
+   .. tacv:: injection @num as {+ intro_pattern}
+   .. tacv:: injection as {+ intro_pattern}
+   .. tacv:: einjection @term {? with @bindings_list} as {+ intro_pattern}
+   .. tacv:: einjection @num as {+ intro_pattern}
+   .. tacv:: einjection as {+ intro_pattern}
 
    These variants apply :n:`intros {+ @intro_pattern}` after the call to
-   ``injection`` or ``einjection`` so that all equalities generated are moved in
+   :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in
    the context of hypotheses. The number of :n:`@intro_pattern` must not exceed
    the number of equalities newly generated. If it is smaller, fresh
    names are automatically generated to adjust the list of :n:`@intro_pattern`
    to the number of new equalities. The original equality is erased if it
    corresponds to an hypothesis.
 
-.. opt:: Structural Injection
+   .. opt:: Structural Injection
 
-   This option ensure that :n:`injection @term` erases the original hypothesis
-   and leaves the generated equalities in the context rather than putting them
-   as antecedents of the current goal, as if giving :n:`injection @term as`
-   (with an empty list of names). This option is off by default.
+      This option ensure that :n:`injection @term` erases the original hypothesis
+      and leaves the generated equalities in the context rather than putting them
+      as antecedents of the current goal, as if giving :n:`injection @term as`
+      (with an empty list of names). This option is off by default.
 
-.. opt:: Keep Proof Equalities
+   .. opt:: Keep Proof Equalities
 
-   By default, :tacn:`injection` only creates new equalities between :n:`@terms`
-   whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special
-   behavior for objects that are proofs of a statement in :g:`Prop`. This option
-   controls this behavior.
+      By default, :tacn:`injection` only creates new equalities between :n:`@terms`
+      whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special
+      behavior for objects that are proofs of a statement in :g:`Prop`. This option
+      controls this behavior.
 
 .. tacn:: inversion @ident
    :name: inversion
@@ -2406,7 +2411,7 @@ Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification,
 and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new
 subgoals.
 
-.. exn:: The @term provided does not end with an equation
+.. exn:: The @term provided does not end with an equation.
 
 .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal.
 
@@ -2430,8 +2435,8 @@ subgoals.
         In particular a failure will happen if any of these three simpler tactics
         fails.
       + :n:`rewrite H in * |-` will do :n:`rewrite H in H`:sub:`i` for all hypotheses
-        :g:`H`:sub:`i` :g:`<> H`. A success will happen as soon as at least one of these
-        simpler tactics succeeds.
+        :g:`H`:sub:`i` different from :g:`H`.
+        A success will happen as soon as at least one of these simpler tactics succeeds.
       + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-`
         that succeeds if at least one of these two tactics succeeds.
 
@@ -2484,7 +2489,7 @@ subgoals.
    the assumption, or if its symmetric form occurs. It is equivalent to
    :n:`cut @term = @term; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`.
 
-.. exn:: @terms do not have convertible types
+.. exn:: @terms do not have convertible types.
 
 .. tacv:: replace @term with @term by tactic
 
@@ -2629,7 +2634,7 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
    with `U` providing that `U` is well-formed and that `T` and `U` are
    convertible.
 
-.. exn:: Not convertible
+.. exn:: Not convertible.
 
 
 .. tacv:: change @term with @term
@@ -2642,7 +2647,7 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
   This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term by @term`
   in the current goal. The terms :n:`@term` and :n:`@term` must be convertible.
 
-.. exn:: Too few occurrences
+.. exn:: Too few occurrences.
 
 .. tacv:: change @term in @ident
 .. tacv:: change @term with @term in @ident
@@ -2817,7 +2822,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    definition (say :g:`t`) and then reduces
    :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules.
 
-.. exn:: Not reducible
+.. exn:: Not reducible.
 
 .. tacn:: hnf
    :name: hnf
@@ -2944,7 +2949,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
    matching :n:`@pattern` in the current goal.
 
-   .. exn:: Too few occurrences
+   .. exn:: Too few occurrences.
 
 .. tacv:: simpl @qualid
 .. tacv:: simpl @string
@@ -2974,7 +2979,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :n:`@qualid` refers in the current goal and then replaces it with its
    :math:`\beta`:math:`\iota`-normal form.
 
-.. exn:: @qualid does not denote an evaluable constant
+.. exn:: @qualid does not denote an evaluable constant.
 
 .. tacv:: unfold @qualid in @ident
 
@@ -2991,9 +2996,9 @@ the conversion in hypotheses :n:`{+ @ident}`.
    The lists :n:`{+, @num}` specify the occurrences of :n:`@qualid` to be
    unfolded. Occurrences are located from left to right.
 
-   .. exn:: bad occurrence number of @qualid
+   .. exn:: Bad occurrence number of @qualid.
 
-   .. exn:: @qualid does not occur
+   .. exn:: @qualid does not occur.
 
 .. tacv:: unfold @string
 
@@ -3083,7 +3088,7 @@ Conversion tactics applied to hypotheses
 
    Example: :n:`unfold not in (Type of H1) (Type of H3)`.
 
-.. exn:: No such hypothesis : ident.
+.. exn:: No such hypothesis: @ident.
 
 
 .. _automation:
@@ -3134,6 +3139,7 @@ hints of the database named core.
    to know what lemmas/assumptions were used.
 
 .. tacv:: debug auto
+   :name: debug auto
 
    Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal,
    including failing paths.
@@ -3153,7 +3159,9 @@ hints of the database named core.
 .. tacv:: trivial with *
 .. tacv:: trivial using {+ @lemma}
 .. tacv:: debug trivial
+   :name: debug trivial
 .. tacv:: info_trivial
+   :name: info_trivial
 .. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}}
 
 .. note::
@@ -3263,7 +3271,8 @@ See also: :tacn:`autorewrite` for examples showing the use of this tactic.
 
    This tactic tries to solve the current goal by a number of standard closing steps.
    In particular, it tries to close the current goal using the closing tactics
-   :tacn:`trivial`, reflexivity, symmetry, contradiction and inversion of hypothesis.
+   :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction`
+   and :tacn:`inversion` of hypothesis.
    If this fails, it tries introducing variables and splitting and-hypotheses,
    using the closing tactics afterwards, and splitting the goal using
    :tacn:`split` and recursing.
@@ -3274,7 +3283,7 @@ See also: :tacn:`autorewrite` for examples showing the use of this tactic.
 .. tacv:: now @tactic
    :name: now
 
-   Run :n:`@tac` followed by ``easy``. This is a notation for :n:`@tactic; easy`.
+   Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`.
 
 Controlling automation
 --------------------------
@@ -3284,40 +3293,42 @@ Controlling automation
 The hints databases for auto and eauto
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The hints for ``auto`` and ``eauto`` are stored in databases. Each database
-maps head symbols to a list of hints. One can use the command
+The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database
+maps head symbols to a list of hints.
 
 .. cmd:: Print Hint @ident
 
-to display the hints associated to the head symbol :n:`@ident`
-(see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative
-integer, and an optional pattern. The hints with lower cost are tried first. A
-hint is tried by ``auto`` when the conclusion of the current goal matches its
-pattern or when it has no pattern.
+   Use this command
+   to display the hints associated to the head symbol :n:`@ident`
+   (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative
+   integer, and an optional pattern. The hints with lower cost are tried first. A
+   hint is tried by :tacn:`auto` when the conclusion of the current goal matches its
+   pattern or when it has no pattern.
 
 Creating Hint databases
 ```````````````````````
 
-One can optionally declare a hint database using the command ``Create
-HintDb``. If a hint is added to an unknown database, it will be
+One can optionally declare a hint database using the command
+:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be
 automatically created.
 
-.. cmd:: Create HintDb @ident {? discriminated}.
-
-This command creates a new database named :n:`@ident`. The database is
-implemented by a Discrimination Tree (DT) that serves as an index of
-all the lemmas. The DT can use transparency information to decide if a
-constant should be indexed or not (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`),
-making the retrieval more efficient. The legacy implementation (the default one
-for new databases) uses the DT only on goals without existentials (i.e., ``auto``
-goals), for non-Immediate hints and do not make use of transparency
-hints, putting more work on the unification that is run after
-retrieval (it keeps a list of the lemmas in case the DT is not used).
-The new implementation enabled by the discriminated option makes use
-of DTs in all cases and takes transparency information into account.
-However, the order in which hints are retrieved from the DT may differ
-from the order in which they were inserted, making this implementation
-observationally different from the legacy one.
+.. cmd:: Create HintDb @ident {? discriminated}
+
+   This command creates a new database named :n:`@ident`. The database is
+   implemented by a Discrimination Tree (DT) that serves as an index of
+   all the lemmas. The DT can use transparency information to decide if a
+   constant should be indexed or not
+   (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`),
+   making the retrieval more efficient. The legacy implementation (the default one
+   for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto`
+   goals), for non-Immediate hints and do not make use of transparency
+   hints, putting more work on the unification that is run after
+   retrieval (it keeps a list of the lemmas in case the DT is not used).
+   The new implementation enabled by the discriminated option makes use
+   of DTs in all cases and takes transparency information into account.
+   However, the order in which hints are retrieved from the DT may differ
+   from the order in which they were inserted, making this implementation
+   observationally different from the legacy one.
 
 The general command to add a hint to some databases :n:`{+ @ident}` is
 
@@ -3341,21 +3352,21 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
    .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}}
       :name: Hint Resolve
 
-   This command adds :n:`simple apply @term` to the hint list with the head
-   symbol of the type of :n:`@term`. The cost of that hint is the number of
-   subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The
-   associated :n:`@pattern` is inferred from the conclusion of the type of
-   :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type
-   of :n:`@term` does not start with a product the tactic added in the hint list
-   is :n:`exact @term`. In case this type can however be reduced to a type
-   starting with a product, the tactic :n:`simple apply @term` is also stored in
-   the hints list. If the inferred type of :n:`@term` contains a dependent
-   quantification on a variable which occurs only in the premisses of the type
-   and not in its conclusion, no instance could be inferred for the variable by
-   unification with the goal. In this case, the hint is added to the hint list
-   of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A
-   typical example of a hint that is used only by :tacn:`eauto` is a transitivity
-   lemma.
+      This command adds :n:`simple apply @term` to the hint list with the head
+      symbol of the type of :n:`@term`. The cost of that hint is the number of
+      subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The
+      associated :n:`@pattern` is inferred from the conclusion of the type of
+      :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type
+      of :n:`@term` does not start with a product the tactic added in the hint list
+      is :n:`exact @term`. In case this type can however be reduced to a type
+      starting with a product, the tactic :n:`simple apply @term` is also stored in
+      the hints list. If the inferred type of :n:`@term` contains a dependent
+      quantification on a variable which occurs only in the premisses of the type
+      and not in its conclusion, no instance could be inferred for the variable by
+      unification with the goal. In this case, the hint is added to the hint list
+      of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A
+      typical example of a hint that is used only by :tacn:`eauto` is a transitivity
+      lemma.
 
    .. exn:: @term cannot be used as a hint
 
@@ -3383,7 +3394,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       This command adds :n:`simple apply @term; trivial` to the hint list associated
       with the head symbol of the type of :n:`@ident` in the given database. This
       tactic will fail if all the subgoals generated by :n:`simple apply @term` are
-      not solved immediately by the ``trivial`` tactic (which only tries tactics
+      not solved immediately by the :tacn:`trivial` tactic (which only tries tactics
       with cost 0).This command is useful for theorems such as the symmetry of
       equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited
       use in order to avoid useless proof-search. The cost of this tactic (which
@@ -3421,7 +3432,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       Adds each :n:`Hint Unfold @ident`.
 
    .. cmdv:: Hint %( Transparent %| Opaque %) @qualid
-      :name: Hint ( Transparent | Opaque )
+      :name: Hint %( Transparent %| Opaque %)
 
       This adds a transparency hint to the database, making :n:`@qualid` a
       transparent or opaque constant during resolution. This information is used
@@ -3429,52 +3440,54 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       discrimination network to relax or constrain it in the case of discriminated
       databases.
 
-    .. cmdv:: Hint %(Transparent | Opaque) {+ @ident}
+   .. cmdv:: Hint %( Transparent %| Opaque %) {+ @ident}
 
       Declares each :n:`@ident` as a transparent or opaque constant.
 
-    .. cmdv:: Hint Extern @num {? @pattern} => tactic
+   .. cmdv:: Hint Extern @num {? @pattern} => tactic
+
+      This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
+      :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
+      :n:`@tactic` to execute.
 
-       This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
-       :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
-       :n:`@tactic` to execute.
+      .. example::
 
-       .. example::
+         .. coqtop:: in
 
-          .. coqtop:: in
+            Hint Extern 4 (~(_ = _)) => discriminate.
 
-             Hint Extern 4 (~(_ = _)) => discriminate.
+         Now, when the head of the goal is a disequality, ``auto`` will try
+         discriminate if it does not manage to solve the goal with hints with a
+         cost less than 4.
 
-       Now, when the head of the goal is a disequality, ``auto`` will try
-       discriminate if it does not manage to solve the goal with hints with a
-       cost less than 4. One can even use some sub-patterns of the pattern in
-       the tactic script. A sub-pattern is a question mark followed by an
-       identifier, like ``?X1`` or ``?X2``. Here is an example:
+      One can even use some sub-patterns of the pattern in
+      the tactic script. A sub-pattern is a question mark followed by an
+      identifier, like ``?X1`` or ``?X2``. Here is an example:
 
-       .. example::
+      .. example::
 
-          .. coqtop:: reset all
+         .. coqtop:: reset all
 
-             Require Import List.
-             Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
-             Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
-             Info 1 auto with eqdec.
+            Require Import List.
+            Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
+            Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
+            Info 1 auto with eqdec.
 
-    .. cmdv:: Hint Cut @regexp
+   .. cmdv:: Hint Cut @regexp
 
-       .. warning::
+      .. warning::
 
-          These hints currently only apply to typeclass proof search and the
-          :tacn:`typeclasses eauto` tactic.
+         These hints currently only apply to typeclass proof search and the
+         :tacn:`typeclasses eauto` tactic.
 
-       This command can be used to cut the proof-search tree according to a regular
-       expression matching paths to be cut. The grammar for regular expressions is
-       the following. Beware, there is no operator precedence during parsing, one can
-       check with :cmd:`Print HintDb` to verify the current cut expression:
+      This command can be used to cut the proof-search tree according to a regular
+      expression matching paths to be cut. The grammar for regular expressions is
+      the following. Beware, there is no operator precedence during parsing, one can
+      check with :cmd:`Print HintDb` to verify the current cut expression:
 
-       .. productionlist:: `regexp`
+      .. productionlist:: `regexp`
           e : ident      hint or instance identifier
-            :|_         any hint
+            :| _         any hint
             :| e\|e′     disjunction
             :| e e′      sequence
             :| e *       Kleene star
@@ -3482,42 +3495,42 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
             :| eps       epsilon
             :| ( e  )
 
-       The `emp` regexp does not match any search path while `eps`
-       matches the empty path. During proof search, the path of
-       successive successful hints on a search branch is recorded, as a
-       list of identifiers for the hints (note Hint Extern’s do not have
-       an associated identifier).
-       Before applying any hint :n:`@ident` the current path `p` extended with
-       :n:`@ident` is matched against the current cut expression `c` associated to
-       the hint database. If matching succeeds, the hint is *not* applied. The
-       semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the
-       initial cut expression being `emp`.
-
-    .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
-
-       This sets an optional mode of use of the identifier :n:`@qualid`. When
-       proof-search faces a goal that ends in an application of :n:`@qualid` to
-       arguments :n:`@term ... @term`, the mode tells if the hints associated to
-       :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``,
-       ``!`` or ``-`` items that specify if an argument of the identifier is to be
-       treated as an input (``+``), if its head only is an input (``!``) or an output
-       (``-``) of the identifier. For a mode to match a list of arguments, input
-       terms and input heads *must not* contain existential variables or be
-       existential variables respectively, while outputs can be any term. Multiple
-       modes can be declared for a single identifier, in that case only one mode
-       needs to match the arguments for the hints to be applied.The head of a term
-       is understood here as the applicative head, or the match or projection
-       scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is
-       especially useful for typeclasses, when one does not want to support default
-       instances and avoid ambiguity in general. Setting a parameter of a class as an
-       input forces proof-search to be driven by that index of the class, with ``!``
-       giving more flexibility by allowing existentials to still appear deeper in the
-       index but not at its head.
-
-    .. note::
-
-       One can use an ``Extern`` hint with no pattern to do pattern-matching on
-       hypotheses using ``match goal`` with inside the tactic.
+      The `emp` regexp does not match any search path while `eps`
+      matches the empty path. During proof search, the path of
+      successive successful hints on a search branch is recorded, as a
+      list of identifiers for the hints (note Hint Extern’s do not have
+      an associated identifier).
+      Before applying any hint :n:`@ident` the current path `p` extended with
+      :n:`@ident` is matched against the current cut expression `c` associated to
+      the hint database. If matching succeeds, the hint is *not* applied. The
+      semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the
+      initial cut expression being `emp`.
+
+   .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
+
+      This sets an optional mode of use of the identifier :n:`@qualid`. When
+      proof-search faces a goal that ends in an application of :n:`@qualid` to
+      arguments :n:`@term ... @term`, the mode tells if the hints associated to
+      :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``,
+      ``!`` or ``-`` items that specify if an argument of the identifier is to be
+      treated as an input (``+``), if its head only is an input (``!``) or an output
+      (``-``) of the identifier. For a mode to match a list of arguments, input
+      terms and input heads *must not* contain existential variables or be
+      existential variables respectively, while outputs can be any term. Multiple
+      modes can be declared for a single identifier, in that case only one mode
+      needs to match the arguments for the hints to be applied.The head of a term
+      is understood here as the applicative head, or the match or projection
+      scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is
+      especially useful for typeclasses, when one does not want to support default
+      instances and avoid ambiguity in general. Setting a parameter of a class as an
+      input forces proof-search to be driven by that index of the class, with ``!``
+      giving more flexibility by allowing existentials to still appear deeper in the
+      index but not at its head.
+
+   .. note::
+
+      One can use an ``Extern`` hint with no pattern to do pattern-matching on
+      hypotheses using ``match goal`` with inside the tactic.
 
 
 Hint databases defined in the Coq standard library
@@ -3639,7 +3652,7 @@ described above: either they disappear at the end of a section scope,
 or they remain global forever. This causes a scalability issue,
 because hints coming from an unrelated part of the code may badly
 influence another development. It can be mitigated to some extent
-thanks to the ``Remove Hints`` command (see :ref:`Remove Hints <removehints>`),
+thanks to the :cmd:`Remove Hints` command,
 but this is a mere workaround and has some limitations (for instance, external
 hints cannot be removed).
 
@@ -3647,7 +3660,7 @@ A proper way to fix this issue is to bind the hints to their module scope, as
 for most of the other objects Coq uses. Hints should only made available when
 the module they are defined in is imported, not just required. It is very
 difficult to change the historical behavior, as it would break a lot of scripts.
-We propose a smooth transitional path by providing the ``Loose Hint Behavior``
+We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior`
 option which accepts three flags allowing for a fine-grained handling of
 non-imported hints.
 
@@ -3857,7 +3870,7 @@ inductive definition.
 
   This combines the effects of the different variants of :tacn:`firstorder`.
 
-.. opt:: Firstorder Depth @natural
+.. opt:: Firstorder Depth @num
 
    This option controls the proof-search depth bound.
 
@@ -3900,11 +3913,12 @@ match against it.
   hypotheses using assert in order for :tacn:`congruence` to use them.
 
 .. tacv:: congruence with {+ @term}
+   :name: congruence with
 
-  Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps
-  in case you have partially applied constructors in your goal.
+   Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps
+   in case you have partially applied constructors in your goal.
 
-.. exn:: I don’t know how to handle dependent equality
+.. exn:: I don’t know how to handle dependent equality.
 
   The decision procedure managed to find a proof of the goal or of a
   discriminable equality but this proof could not be built in Coq because of
@@ -3916,7 +3930,7 @@ match against it.
   arguments are supplied for some partially applied constructors. Any term of an
   appropriate type will allow the tactic to successfully solve the goal. Those
   additional arguments can be given to congruence by filling in the holes in the
-  terms given in the error message, using the with variant described above.
+  terms given in the error message, using the :tacn:`congruence with` variant described above.
 
 .. opt:: Congruence Verbose
 
@@ -3935,7 +3949,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its arguments are equal modulo alpha
    conversion and casts.
 
-.. exn:: Not equal
+.. exn:: Not equal.
 
 .. tacn:: unify @term @term
    :name: unify
@@ -3943,7 +3957,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its arguments are unifiable, potentially
    instantiating existential variables.
 
-.. exn:: Not unifiable
+.. exn:: Not unifiable.
 
 .. tacv:: unify @term @term with @ident
 
@@ -3957,7 +3971,7 @@ succeeds, and results in an error otherwise.
    variable. Existential variables are uninstantiated variables generated
    by :tacn:`eapply` and some other tactics.
 
-.. exn:: Not an evar
+.. exn:: Not an evar.
 
 .. tacn:: has_evar @term
    :name: has_evar
@@ -3966,7 +3980,7 @@ succeeds, and results in an error otherwise.
    a subterm. Unlike context patterns combined with ``is_evar``, this tactic
    scans all subterms, including those under binders.
 
-.. exn:: No evars
+.. exn:: No evars.
 
 .. tacn:: is_var @term
    :name: is_var
@@ -3974,7 +3988,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its argument is a variable or hypothesis in
    the current goal context or in the opened sections.
 
-.. exn:: Not a variable or hypothesis
+.. exn:: Not a variable or hypothesis.
 
 
 .. _equality:
@@ -4001,7 +4015,7 @@ This tactic applies to a goal that has the form :g:`t=u`. It checks that `t`
 and `u` are convertible and then solves the goal. It is equivalent to apply
 :tacn:`refl_equal`.
 
-.. exn:: The conclusion is not a substitutive equation
+.. exn:: The conclusion is not a substitutive equation.
 
 .. exn:: Unable to unify ... with ...
 
@@ -4119,8 +4133,8 @@ Inversion
 available after a ``Require Import FunInd``.
 
 
-.. exn:: Hypothesis @ident must contain at least one Function
-.. exn:: Cannot find inversion information for hypothesis @ident
+.. exn:: Hypothesis @ident must contain at least one Function.
+.. exn:: Cannot find inversion information for hypothesis @ident.
 
   This error may be raised when some inversion lemma failed to be generated by
   Function.
@@ -4151,7 +4165,7 @@ function :n:`@ident`. This function must be a fixpoint on a simple recursive
 datatype: see :ref:`quote` for the full details.
 
 
-.. exn:: quote: not a simple fixpoint
+.. exn:: quote: not a simple fixpoint.
 
   Happens when quote is not able to perform inversion properly.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 692ff294a6..7ba103b222 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -14,64 +14,63 @@ Displaying
 
 .. _Print:
 
-.. cmd:: Print @qualid.
+.. cmd:: Print @qualid
+   :name: Print
 
-This command displays on the screen information about the declared or
-defined object referred by :n:`@qualid`.
+   This command displays on the screen information about the declared or
+   defined object referred by :n:`@qualid`.
 
+   Error messages:
 
-Error messages:
+   .. exn:: @qualid not a defined object.
 
+   .. exn:: Universe instance should have length @num.
 
-.. exn:: @qualid not a defined object
+   .. exn:: This object does not support universe names.
 
-.. exn:: Universe instance should have length :n:`num`.
 
-.. exn:: This object does not support universe names.
+   .. cmdv:: Print Term @qualid
+      :name: Print Term
 
+      This is a synonym of :cmd:`Print` :n:`@qualid` when :n:`@qualid`
+      denotes a global constant.
 
-Variants:
+   .. cmdv:: Print {? Term } @qualid\@@name
 
+      This locally renames the polymorphic universes of :n:`@qualid`.
+      An underscore means the raw universe is printed.
 
-.. cmdv:: Print Term @qualid.
 
-This is a synonym to ``Print`` :n:`@qualid` when :n:`@qualid`
-denotes a global constant.
-
-.. cmdv:: About @qualid.
+.. cmd:: About @qualid
    :name: About
 
-This displays various information about the object
-denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive,
-constructor, abbreviation, …), long name, type, implicit arguments and
-argument scopes. It does not print the body of definitions or proofs.
-
-.. cmdv:: Print @qualid\@@name
+   This displays various information about the object
+   denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive,
+   constructor, abbreviation, …), long name, type, implicit arguments and
+   argument scopes. It does not print the body of definitions or proofs.
 
-This locally renames the polymorphic universes of :n:`@qualid`.
-An underscore means the raw universe is printed.
-This form can be used with ``Print Term`` and ``About``.
+   .. cmdv:: About @qualid\@@name
 
-.. cmd:: Print All.
+      This locally renames the polymorphic universes of :n:`@qualid`.
+      An underscore means the raw universe is printed.
 
-This command displays information about the current state of the
-environment, including sections and modules.
 
+.. cmd:: Print All
 
-Variants:
+   This command displays information about the current state of the
+   environment, including sections and modules.
 
+   .. cmdv:: Inspect @num
+      :name: Inspect
 
-.. cmdv:: Inspect @num.
-   :name: Inspect
+      This command displays the :n:`@num` last objects of the
+      current environment, including sections and modules.
 
-This command displays the :n:`@num` last objects of the
-current environment, including sections and modules.
+   .. cmdv:: Print Section @ident
 
-.. cmdv:: Print Section @ident.
-
-The name :n:`@ident` should correspond to a currently open section,
-this command displays the objects defined since the beginning of this
-section.
+      The name :n:`@ident` should correspond to a currently open section,
+      this command displays the objects defined since the beginning of this
+      section.
 
 
 .. _flags-options-tables:
@@ -87,151 +86,136 @@ handling flags, options and tables are given below.
 
 .. TODO : flag is not a syntax entry
 
-.. cmd:: Set @flag.
-
-This command switches :n:`@flag` on. The original state of :n:`@flag` is restored
-when the current module ends.
-
-Variants:
-
-.. cmdv:: Local Set @flag.
-
-This command switches :n:`@flag` on. The original state
-of :n:`@flag` is restored when the current *section* ends.
+.. cmd:: Set @flag
 
-.. cmdv:: Global Set @flag.
+   This command switches :n:`@flag` on. The original state of :n:`@flag`
+   is restored when the current module ends.
 
-This command switches :n:`@flag` on. The original state
-of :n:`@flag` is *not* restored at the end of the module. Additionally, if
-set in a file, :n:`@flag` is switched on when the file is `Require`-d.
+   .. cmdv:: Local Set @flag
 
-.. cmdv:: Export Set @flag.
+      This command switches :n:`@flag` on. The original state
+      of :n:`@flag` is restored when the current *section* ends.
 
-   This command switches :n:`@flag` on. The original state
-   of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
-   is switched on when this module is imported.
+   .. cmdv:: Global Set @flag
 
+      This command switches :n:`@flag` on. The original state
+      of :n:`@flag` is *not* restored at the end of the module. Additionally, if
+      set in a file, :n:`@flag` is switched on when the file is `Require`-d.
 
-.. cmd:: Unset @flag.
+   .. cmdv:: Export Set @flag
 
-This command switches :n:`@flag` off. The original state of :n:`@flag` is restored
-when the current module ends.
+      This command switches :n:`@flag` on. The original state
+      of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
+      is switched on when this module is imported.
 
 
-Variants:
+.. cmd:: Unset @flag
 
-.. cmdv:: Local Unset @flag.
+   This command switches :n:`@flag` off. The original state of
+   :n:`@flag` is restored when the current module ends.
 
-This command switches :n:`@flag` off. The original
-state of :n:`@flag` is restored when the current *section* ends.
+   .. cmdv:: Local Unset @flag
 
-.. cmdv:: Global Unset @flag.
+      This command switches :n:`@flag` off. The original
+      state of :n:`@flag` is restored when the current *section* ends.
 
-This command switches :n:`@flag` off. The original
-state of :n:`@flag` is *not* restored at the end of the module. Additionally,
-if set in a file, :n:`@flag` is switched off when the file is `Require`-d.
+   .. cmdv:: Global Unset @flag
 
-.. cmdv:: Export Unset @flag.
+      This command switches :n:`@flag` off. The original
+      state of :n:`@flag` is *not* restored at the end of the module. Additionally,
+      if set in a file, :n:`@flag` is switched off when the file is `Require`-d.
 
-   This command switches :n:`@flag` off. The original state
-   of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
-   is switched off when this module is imported.
+   .. cmdv:: Export Unset @flag
 
+      This command switches :n:`@flag` off. The original state
+      of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
+      is switched off when this module is imported.
 
-.. cmd:: Test @flag.
 
-This command prints whether :n:`@flag` is on or off.
+.. cmd:: Test @flag
 
+   This command prints whether :n:`@flag` is on or off.
 
-.. cmd:: Set @option @value.
 
-This command sets :n:`@option` to :n:`@value`. The original value of ` option` is
-restored when the current module ends.
+.. cmd:: Set @option @value
 
+   This command sets :n:`@option` to :n:`@value`. The original value of ` option` is
+   restored when the current module ends.
 
-Variants:
+   .. TODO : option and value are not syntax entries
 
-.. TODO : option and value are not syntax entries
+   .. cmdv:: Local Set @option @value
 
-.. cmdv:: Local Set @option @value.
+      This command sets :n:`@option` to :n:`@value`. The
+      original value of :n:`@option` is restored at the end of the module.
 
-This command sets :n:`@option` to :n:`@value`. The
-original value of :n:`@option` is restored at the end of the module.
+   .. cmdv:: Global Set @option @value
 
-.. cmdv:: Global Set @option @value.
+      This command sets :n:`@option` to :n:`@value`. The
+      original value of :n:`@option` is *not* restored at the end of the module.
+      Additionally, if set in a file, :n:`@option` is set to value when the file
+      is `Require`-d.
 
-This command sets :n:`@option` to :n:`@value`. The
-original value of :n:`@option` is *not* restored at the end of the module.
-Additionally, if set in a file, :n:`@option` is set to value when the file
-is `Require`-d.
+   .. cmdv:: Export Set @option
 
-.. cmdv:: Export Set @option.
+      This command set :n:`@option` to :n:`@value`. The original state
+      of :n:`@option` is restored at the end of the current module, but :n:`@option`
+      is set to :n:`@value` when this module is imported.
 
-   This command set :n:`@option` to :n:`@value`. The original state
-   of :n:`@option` is restored at the end of the current module, but :n:`@option`
-   is set to :n:`@value` when this module is imported.
 
-
-.. cmd::  Unset @option.
+.. cmd:: Unset @option
 
    This command turns off :n:`@option`.
 
+   .. cmdv:: Local Unset @option
 
-Variants:
-
+      This command turns off :n:`@option`. The original state of :n:`@option`
+      is restored when the current *section* ends.
 
-.. cmdv:: Local Unset @option.
+   .. cmdv:: Global Unset @option
 
-   This command turns off :n:`@option`. The original state of :n:`@option` is restored when the current
-   *section* ends.
+      This command turns off :n:`@option`. The original state of :n:`@option`
+      is *not* restored at the end of the module. Additionally, if unset in a file,
+      :n:`@option` is reset to its default value when the file is `Require`-d.
 
-.. cmdv:: Global Unset @option.
+   .. cmdv:: Export Unset @option
 
-   This command turns off :n:`@option`. The original state of :n:`@option` is *not* restored at the end of the
-   module. Additionally, if unset in a file, :n:`@option` is reset to its
-   default value when the file is `Require`-d.
+      This command turns off :n:`@option`. The original state of :n:`@option`
+      is restored at the end of the current module, but :n:`@option` is set to
+      its default value when this module is imported.
 
-.. cmdv:: Export Unset @option.
-
-   This command turns off :n:`@option`. The original state of :n:`@option` is restored at the end of the
-   current module, but :n:`@option` is set to its default value when this module
-   is imported.
 
+.. cmd:: Test @option
 
-.. cmd:: Test @option.
-
-This command prints the current value of :n:`@option`.
+   This command prints the current value of :n:`@option`.
 
 
 .. TODO : table is not a syntax entry
 
-.. cmd:: Add @table @value.
+.. cmd:: Add @table @value
    :name: Add `table` `value`
 
-.. cmd:: Remove @table @value.
+.. cmd:: Remove @table @value
    :name: Remove `table` `value`
 
-.. cmd:: Test @table @value.
+.. cmd:: Test @table @value
    :name: Test `table` `value`
 
-.. cmd:: Test @table for @value.
+.. cmd:: Test @table for @value
    :name: Test `table` for `value`
 
-.. cmd:: Print Table @table.
-
-These are  general commands for tables.
-
-.. cmd:: Print Options.
+.. cmd:: Print Table @table
 
-This command lists all available flags, options and tables.
+These are general commands for tables.
 
 
-Variants:
+.. cmd:: Print Options
 
+   This command lists all available flags, options and tables.
 
-.. cmdv:: Print Tables.
+   .. cmdv:: Print Tables
 
-This is a synonymous of ``Print Options``.
+      This is a synonymous of :cmd:`Print Options`.
 
 
 .. _requests-to-the-environment:
@@ -239,358 +223,330 @@ This is a synonymous of ``Print Options``.
 Requests to the environment
 -------------------------------
 
-.. cmd:: Check @term.
+.. cmd:: Check @term
 
-This command displays the type of :n:`@term`. When called in proof mode, the
-term is checked in the local context of the current subgoal.
+   This command displays the type of :n:`@term`. When called in proof mode, the
+   term is checked in the local context of the current subgoal.
 
 
-Variants:
+   .. TODO : selector is not a syntax entry
 
-.. TODO : selector is not a syntax entry
+   .. cmdv:: @selector: Check @term
 
-.. cmdv:: @selector: Check @term.
+      This variant specifies on which subgoal to perform typing
+      (see Section :ref:`invocation-of-tactics`).
 
-specifies on which subgoal to perform typing
-(see Section :ref:`invocation-of-tactics`).
 
 .. TODO : convtactic is not a syntax entry
 
-.. cmd:: Eval @convtactic in @term.
-
-This command performs the specified reduction on :n:`@term`, and displays
-the resulting term with its type. The term to be reduced may depend on
-hypothesis introduced in the first subgoal (if a proof is in
-progress).
-
-
-See also: Section :ref:`performingcomputations`.
-
-
-.. cmd:: Compute @term.
-
-This command performs a call-by-value evaluation of term by using the
-bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in``
-:n:`@term`.
-
-
-See also: Section :ref:`performingcomputations`.
-
-
-.. cmd::Extraction @term.
-
-This command displays the extracted term from :n:`@term`. The extraction is
-processed according to the distinction between :g:`Set` and :g:`Prop`; that is
-to say, between logical and computational content (see Section :ref:`sorts`).
-The extracted term is displayed in OCaml syntax, where global identifiers are
-still displayed as in |Coq| terms.
-
-
-Variants:
+.. cmd:: Eval @convtactic in @term
 
+   This command performs the specified reduction on :n:`@term`, and displays
+   the resulting term with its type. The term to be reduced may depend on
+   hypothesis introduced in the first subgoal (if a proof is in
+   progress).
 
-.. cmdv:: Recursive Extraction {+ @qualid }.
+   See also: Section :ref:`performingcomputations`.
 
-Recursively extracts all
-the material needed for the extraction of the qualified identifiers.
 
+.. cmd:: Compute @term
 
-See also: Chapter :ref:`extraction`.
+   This command performs a call-by-value evaluation of term by using the
+   bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in``
+   :n:`@term`.
 
+   See also: Section :ref:`performingcomputations`.
 
-.. cmd:: Print Assumptions @qualid.
 
-This commands display all the assumptions (axioms, parameters and
-variables) a theorem or definition depends on. Especially, it informs
-on the assumptions with respect to which the validity of a theorem
-relies.
+.. cmd:: Print Assumptions @qualid
 
+   This commands display all the assumptions (axioms, parameters and
+   variables) a theorem or definition depends on. Especially, it informs
+   on the assumptions with respect to which the validity of a theorem
+   relies.
 
-Variants:
+   .. cmdv:: Print Opaque Dependencies @qualid
+      :name: Print Opaque Dependencies
 
+      Displays the set of opaque constants :n:`@qualid` relies on in addition to
+      the assumptions.
 
-.. cmdv:: Print Opaque Dependencies @qualid.
+   .. cmdv:: Print Transparent Dependencies @qualid
+      :name: Print Transparent Dependencies
 
-Displays the set of opaque constants :n:`@qualid` relies on in addition to
-the assumptions.
+      Displays the set of transparent constants :n:`@qualid` relies on
+      in addition to the assumptions.
 
-.. cmdv:: Print Transparent Dependencies @qualid.
+   .. cmdv:: Print All Dependencies @qualid
+      :name: Print All Dependencies
 
-Displays the set of
-transparent constants :n:`@qualid` relies on in addition to the assumptions.
+      Displays all assumptions and constants :n:`@qualid` relies on.
 
-.. cmdv:: Print All Dependencies @qualid.
 
-Displays all assumptions and constants :n:`@qualid` relies on.
+.. cmd:: Search @qualid
 
+   This command displays the name and type of all objects (hypothesis of
+   the current goal, theorems, axioms, etc) of the current context whose
+   statement contains :n:`@qualid`. This command is useful to remind the user
+   of the name of library lemmas.
 
+   .. exn:: The reference @qualid was not found in the current environment.
 
-.. cmd:: Search @qualid.
+      There is no constant in the environment named qualid.
 
-This command displays the name and type of all objects (hypothesis of
-the current goal, theorems, axioms, etc) of the current context whose
-statement contains :n:`@qualid`. This command is useful to remind the user
-of the name of library lemmas.
+   .. cmdv:: Search @string
 
+      If :n:`@string` is a valid identifier, this command
+      displays the name and type of all objects (theorems, axioms, etc) of
+      the current context whose name contains string. If string is a
+      notation’s string denoting some reference :n:`@qualid` (referred to by its
+      main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or
+      `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`.
 
-Error messages:
+   .. cmdv:: Search @string%@key
 
+      The string string must be a notation or the main
+      symbol of a notation which is then interpreted in the scope bound to
+      the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`).
 
-.. exn:: The reference @qualid was not found in the current environment
+   .. cmdv:: Search @term_pattern
 
-There is no constant in the environment named qualid.
+      This searches for all statements or types of
+      definition that contains a subterm that matches the pattern
+      `term_pattern` (holes of the pattern are either denoted by `_` or by
+      `?ident` when non linear patterns are expected).
 
-Variants:
+   .. cmdv:: Search { + [-]@term_pattern_string }
 
-.. cmdv:: Search @string.
+      where
+      :n:`@term_pattern_string` is a term_pattern, a string, or a string followed
+      by a scope delimiting key `%key`.  This generalization of ``Search`` searches
+      for all objects whose statement or type contains a subterm matching
+      :n:`@term_pattern` (or :n:`@qualid` if :n:`@string` is the notation for a reference
+      qualid) and whose name contains all string of the request that
+      correspond to valid identifiers. If a term_pattern or a string is
+      prefixed by `-`, the search excludes the objects that mention that
+      term_pattern or that string.
 
-If :n:`@string` is a valid identifier, this command
-displays the name and type of all objects (theorems, axioms, etc) of
-the current context whose name contains string. If string is a
-notation’s string denoting some reference :n:`@qualid` (referred to by its
-main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or
-`"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`.
+   .. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid }
 
-.. cmdv:: Search @string%@key.
+      This restricts the search to constructions defined in the modules
+      named by the given :n:`qualid` sequence.
 
-The string string must be a notation or the main
-symbol of a notation which is then interpreted in the scope bound to
-the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`).
+   .. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }
 
-.. cmdv:: Search @term_pattern.
+      This restricts the search to constructions not defined in the modules
+      named by the given :n:`qualid` sequence.
 
-This searches for all statements or types of
-definition that contains a subterm that matches the pattern
-`term_pattern` (holes of the pattern are either denoted by `_` or by
-`?ident` when non linear patterns are expected).
+   .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string
 
-.. cmdv:: Search { + [-]@term_pattern_string }.
+      This specifies the goal on which to search hypothesis (see
+      Section :ref:`invocation-of-tactics`).
+      By default the 1st goal is searched. This variant can
+      be combined with other variants presented here.
 
-where
-:n:`@term_pattern_string` is a term_pattern, a string, or a string followed
-by a scope delimiting key `%key`.  This generalization of ``Search`` searches
-for all objects whose statement or type contains a subterm matching
-:n:`@term_pattern` (or :n:`@qualid` if :n:`@string` is the notation for a reference
-qualid) and whose name contains all string of the request that
-correspond to valid identifiers. If a term_pattern or a string is
-prefixed by `-`, the search excludes the objects that mention that
-term_pattern or that string.
+      .. example::
 
-.. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid } .
+         .. coqtop:: in
 
-This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
+            Require Import ZArith.
 
-.. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }.
+         .. coqtop:: all
 
-This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
+            Search Z.mul Z.add "distr".
 
-.. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string.
+            Search "+"%Z "*"%Z "distr" -positive -Prop.
 
-This specifies the goal on which to search hypothesis (see
-Section :ref:`invocation-of-tactics`).
-By default the 1st goal is searched. This variant can
-be combined with other variants presented here.
+            Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 
+   .. cmdv:: SearchAbout
 
-.. coqtop:: in
+      .. deprecated:: 8.5
 
-   Require Import ZArith.
+      Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current
+      :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with
+      command :cmd:`SearchAbout`. For compatibility, the deprecated name
+      :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For
+      compatibility, the list of objects to search when using :cmd:`SearchAbout`
+      may also be enclosed by optional ``[ ]`` delimiters.
 
-.. coqtop:: all
 
-   Search Z.mul Z.add "distr".
+.. cmd:: SearchHead @term
 
-   Search "+"%Z "*"%Z "distr" -positive -Prop.
+   This command displays the name and type of all hypothesis of the
+   current goal (if any) and theorems of the current context whose
+   statement’s conclusion has the form `(term t1 .. tn)`. This command is
+   useful to remind the user of the name of library lemmas.
 
-   Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
+   .. example::
 
-.. note:: Up to |Coq| version 8.4, ``Search`` had the behavior of current
-   ``SearchHead`` and the behavior of current Search was obtained with
-   command ``SearchAbout``. For compatibility, the deprecated name
-   SearchAbout can still be used as a synonym of Search. For
-   compatibility, the list of objects to search when using ``SearchAbout``
-   may also be enclosed by optional ``[ ]`` delimiters.
+      .. coqtop:: reset all
 
+         SearchHead le.
 
-.. cmd:: SearchHead @term.
+         SearchHead (@eq bool).
 
-This command displays the name and type of all hypothesis of the
-current goal (if any) and theorems of the current context whose
-statement’s conclusion has the form `(term t1 .. tn)`. This command is
-useful to remind the user of the name of library lemmas.
+   .. cmdv:: SearchHead @term inside {+ @qualid }
 
+      This restricts the search to constructions defined in the modules named
+      by the given :n:`qualid` sequence.
 
+   .. cmdv:: SearchHead term outside {+ @qualid }
 
-.. coqtop:: reset all
+      This restricts the search to constructions not defined in the modules
+      named by the given :n:`qualid` sequence.
 
-   SearchHead le.
+   .. exn:: Module/section @qualid not found.
 
-   SearchHead (@eq bool).
+      No module :n:`@qualid` has been required (see Section :ref:`compiled-files`).
 
+   .. cmdv:: @selector: SearchHead @term
 
-Variants:
+      This specifies the goal on which to
+      search hypothesis (see Section :ref:`invocation-of-tactics`).
+      By default the 1st goal is searched. This variant can be combined
+      with other variants presented here.
 
-.. cmdv:: SearchHead @term inside {+ @qualid }.
+   .. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``.
 
-This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: SearchHead term outside {+ @qualid }.
+.. cmd:: SearchPattern @term
 
-This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
+   This command displays the name and type of all hypothesis of the
+   current goal (if any) and theorems of the current context whose
+   statement’s conclusion or last hypothesis and conclusion matches the
+   expressionterm where holes in the latter are denoted by `_`.
+   It is a variant of Search @term_pattern that does not look for subterms
+   but searches for statements whose conclusion has exactly the expected
+   form, or whose statement finishes by the given series of
+   hypothesis/conclusion.
 
-Error messages:
+   .. example::
 
-.. exn:: Module/section @qualid not found
+      .. coqtop:: in
 
-No module :n:`@qualid` has been required
-(see Section :ref:`compiled-files`).
+         Require Import Arith.
 
-.. cmdv:: @selector: SearchHead @term.
+      .. coqtop:: all
 
-This specifies the goal on which to
-search hypothesis (see Section :ref:`invocation-of-tactics`).
-By default the 1st goal is
-searched. This variant can be combined with other variants presented
-here.
+         SearchPattern (_ + _ = _ + _).
 
-.. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``.
+         SearchPattern (nat -> bool).
 
+         SearchPattern (forall l : list _, _ l l).
 
-.. cmd:: SearchPattern @term.
+   Patterns need not be linear: you can express that the same expression
+   must occur in two places by using pattern variables `?ident`.
 
-This command displays the name and type of all hypothesis of the
-current goal (if any) and theorems of the current context whose
-statement’s conclusion or last hypothesis and conclusion matches the
-expressionterm where holes in the latter are denoted by `_`.
-It is a
-variant of Search @term_pattern that does not look for subterms but
-searches for statements whose conclusion has exactly the expected
-form, or whose statement finishes by the given series of
-hypothesis/conclusion.
 
-.. coqtop:: in
+   .. example::
 
-   Require Import Arith.
+      .. coqtop:: all
 
-.. coqtop:: all
+         SearchPattern (?X1 + _ = _ + ?X1).
 
-    SearchPattern (_ + _ = _ + _).
+   .. cmdv:: SearchPattern @term inside {+ @qualid }
 
-    SearchPattern (nat -> bool).
+      This restricts the search to constructions defined in the modules
+      named by the given :n:`qualid` sequence.
 
-    SearchPattern (forall l : list _, _ l l).
+   .. cmdv:: SearchPattern @term outside {+ @qualid }
 
-Patterns need not be linear: you can express that the same expression
-must occur in two places by using pattern variables `?ident`.
+      This restricts the search to constructions not defined in the modules
+      named by the given :n:`qualid` sequence.
 
+   .. cmdv:: @selector: SearchPattern @term
 
-.. coqtop:: all
+      This specifies the goal on which to
+      search hypothesis (see Section :ref:`invocation-of-tactics`).
+      By default the 1st goal is
+      searched. This variant can be combined with other variants presented
+      here.
 
-   SearchPattern (?X1 + _ = _ + ?X1).
 
-Variants:
+.. cmd:: SearchRewrite @term
 
+   This command displays the name and type of all hypothesis of the
+   current goal (if any) and theorems of the current context whose
+   statement’s conclusion is an equality of which one side matches the
+   expression term. Holes in term are denoted by “_”.
 
-.. cmdv:: SearchPattern @term inside {+ @qualid } .
+   .. example::
 
-This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
+      .. coqtop:: in
 
-.. cmdv:: SearchPattern @term outside {+ @qualid }.
+         Require Import Arith.
 
-This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
+      .. coqtop:: all
 
-.. cmdv:: @selector: SearchPattern @term.
+         SearchRewrite (_ + _ + _).
 
-This specifies the goal on which to
-search hypothesis (see Section :ref:`invocation-of-tactics`). By default the 1st goal is
-searched. This variant can be combined with other variants presented
-here.
+   .. cmdv:: SearchRewrite term inside {+ @qualid }
 
+      This restricts the search to constructions defined in the modules
+      named by the given :n:`qualid` sequence.
 
+   .. cmdv:: SearchRewrite @term outside {+ @qualid }
 
-.. cmdv:: SearchRewrite @term.
+      This restricts the search to constructions not defined in the modules
+      named by the given :n:`qualid` sequence.
 
-This command displays the name and type of all hypothesis of the
-current goal (if any) and theorems of the current context whose
-statement’s conclusion is an equality of which one side matches the
-expression term. Holes in term are denoted by “_”.
+   .. cmdv:: @selector: SearchRewrite @term
 
-.. coqtop:: in
-
-    Require Import Arith.
-
-.. coqtop:: all
-
-    SearchRewrite (_ + _ + _).
-
-Variants:
-
-
-.. cmdv:: SearchRewrite term inside {+ @qualid }.
-
-This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
-
-.. cmdv:: SearchRewrite @term outside {+ @qualid }.
-
-This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
-
-.. cmdv:: @selector: SearchRewrite @term.
-
-This specifies the goal on which to
-search hypothesis (see Section :ref:`invocation-of-tactics`). By default the 1st goal is
-searched. This variant can be combined with other variants presented
-here.
+      This specifies the goal on which to
+      search hypothesis (see Section :ref:`invocation-of-tactics`).
+      By default the 1st goal is
+      searched. This variant can be combined with other variants presented
+      here.
 
 .. note::
 
-   For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite``
-   queries, it
-   is possible to globally filter the search results via the command
-   ``Add Search Blacklist`` :n:`@substring`. A lemma whose fully-qualified name
-   contains any of the declared substrings will be removed from the
-   search results. The default blacklisted substrings are ``_subproof``
-   ``Private_``. The command ``Remove Search Blacklist ...`` allows expunging
-   this blacklist.
-
+   .. cmd:: Add Search Blacklist @string
 
-.. cmd:: Locate @qualid.
+      For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite``
+      queries, it is possible to globally filter the search results using this
+      command. A lemma whose fully-qualified name
+      contains any of the declared strings will be removed from the
+      search results. The default blacklisted substrings are ``_subproof`` and
+      ``Private_``.
 
-This command displays the full name of objects whose name is a prefix
-of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in
-which they are defined. It searches for objects from the different
-qualified name spaces of |Coq|: terms, modules, Ltac, etc.
+   .. cmd:: Remove Search Blacklist @string
 
-.. coqtop:: none
+      This command allows expunging this blacklist.
 
-    Set Printing Depth 50.
 
-.. coqtop:: all
+.. cmd:: Locate @qualid
 
-    Locate nat.
+   This command displays the full name of objects whose name is a prefix
+   of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in
+   which they are defined. It searches for objects from the different
+   qualified name spaces of |Coq|: terms, modules, Ltac, etc.
 
-    Locate Datatypes.O.
+   .. example::
 
-    Locate Init.Datatypes.O.
+      .. coqtop:: all
 
-    Locate Coq.Init.Datatypes.O.
+         Locate nat.
 
-    Locate I.Dont.Exist.
+         Locate Datatypes.O.
 
-Variants:
+         Locate Init.Datatypes.O.
 
+         Locate Coq.Init.Datatypes.O.
 
-.. cmdv:: Locate Term @qualid.
+         Locate I.Dont.Exist.
 
-As Locate but restricted to terms.
+   .. cmdv:: Locate Term @qualid
 
-.. cmdv:: Locate Module @qualid.
+      As Locate but restricted to terms.
 
-As Locate but restricted to modules.
+   .. cmdv:: Locate Module @qualid
 
-.. cmdv:: Locate Ltac @qualid.
+      As Locate but restricted to modules.
 
-As Locate but restricted to tactics.
+   .. cmdv:: Locate Ltac @qualid
 
+      As Locate but restricted to tactics.
 
 See also: Section :ref:`locating-notations`
 
@@ -608,40 +564,35 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
 (and default) extension of |Coq|’s script files is .v.
 
 
-.. cmd:: Load @ident.
-
-This command loads the file named :n:`ident`.v, searching successively in
-each of the directories specified in the *loadpath*. (see Section
-:ref:`libraries-and-filesystem`)
+.. cmd:: Load @ident
 
-Files loaded this way cannot leave proofs open, and the ``Load``
-command cannot be used inside a proof either.
+   This command loads the file named :n:`ident`.v, searching successively in
+   each of the directories specified in the *loadpath*. (see Section
+   :ref:`libraries-and-filesystem`)
 
-Variants:
+   Files loaded this way cannot leave proofs open, and the ``Load``
+   command cannot be used inside a proof either.
 
+   .. cmdv:: Load @string
 
-.. cmdv:: Load @string.
+      Loads the file denoted by the string :n:`@string`, where
+      string is any complete filename. Then the `~` and .. abbreviations are
+      allowed as well as shell variables. If no extension is specified, |Coq|
+      will use the default extension ``.v``.
 
-Loads the file denoted by the string :n:`@string`, where
-string is any complete filename. Then the `~` and .. abbreviations are
-allowed as well as shell variables. If no extension is specified, |Coq|
-will use the default extension ``.v``.
+   .. cmdv:: Load Verbose @ident
 
-.. cmdv:: Load Verbose @ident.
+   .. cmdv:: Load Verbose @string
 
-.. cmdv:: Load Verbose @string.
+      Display, while loading,
+      the answers of |Coq| to each command (including tactics) contained in
+      the loaded file See also: Section :ref:`controlling-display`.
 
-Display, while loading,
-the answers of |Coq| to each command (including tactics) contained in
-the loaded file See also: Section :ref:`controlling-display`.
+   .. exn:: Can’t find file @ident on loadpath.
 
-Error messages:
+   .. exn:: Load is not supported inside proofs.
 
-.. exn:: Can’t find file @ident on loadpath
-
-.. exn:: Load is not supported inside proofs
-
-.. exn:: Files processed by Load cannot leave open proofs
+   .. exn:: Files processed by Load cannot leave open proofs.
 
 .. _compiled-files:
 
@@ -653,151 +604,137 @@ Chapter :ref:`thecoqcommands` for documentation on how to compile a file). A com
 file is a particular case of module called *library file*.
 
 
-.. cmd:: Require @qualid.
-
-This command looks in the loadpath for a file containing module :n:`@qualid`
-and adds the corresponding module to the environment of |Coq|. As
-library files have dependencies in other library files, the command
-``Require`` :n:`@qualid` recursively requires all library files the module
-qualid depends on and adds the corresponding modules to the
-environment of |Coq| too. |Coq| assumes that the compiled files have been
-produced by a valid |Coq| compiler and their contents are then not
-replayed nor rechecked.
-
-To locate the file in the file system, :n:`@qualid` is decomposed under the
-form `dirpath.ident` and the file `ident.vo` is searched in the physical
-directory of the file system that is mapped in |Coq| loadpath to the
-logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between
-physical directories and logical names at the time of requiring the
-file must be consistent with the mapping used to compile the file. If
-several files match, one of them is picked in an unspecified fashion.
+.. cmd:: Require @qualid
 
+   This command looks in the loadpath for a file containing module :n:`@qualid`
+   and adds the corresponding module to the environment of |Coq|. As
+   library files have dependencies in other library files, the command
+   :cmd:`Require` :n:`@qualid` recursively requires all library files the module
+   qualid depends on and adds the corresponding modules to the
+   environment of |Coq| too. |Coq| assumes that the compiled files have been
+   produced by a valid |Coq| compiler and their contents are then not
+   replayed nor rechecked.
 
-Variants:
+   To locate the file in the file system, :n:`@qualid` is decomposed under the
+   form `dirpath.ident` and the file `ident.vo` is searched in the physical
+   directory of the file system that is mapped in |Coq| loadpath to the
+   logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between
+   physical directories and logical names at the time of requiring the
+   file must be consistent with the mapping used to compile the file. If
+   several files match, one of them is picked in an unspecified fashion.
 
-.. cmdv:: Require Import @qualid.
 
-This loads and declares the module :n:`@qualid`
-and its dependencies then imports the contents of :n:`@qualid` as described
-:ref:`here <import_qualid>`. It does not import the modules on which
-qualid depends unless these modules were themselves required in module
-:n:`@qualid`
-using ``Require Export``, as described below, or recursively required
-through a sequence of ``Require Export``.  If the module required has
-already been loaded, ``Require Import`` :n:`@qualid` simply imports it, as ``Import``
-:n:`@qualid` would.
+   .. cmdv:: Require Import @qualid
 
-.. cmdv:: Require Export @qualid.
+      This loads and declares the module :n:`@qualid`
+      and its dependencies then imports the contents of :n:`@qualid` as described
+      :ref:`here <import_qualid>`. It does not import the modules on which
+      qualid depends unless these modules were themselves required in module
+      :n:`@qualid`
+      using :cmd:`Require Export`, as described below, or recursively required
+      through a sequence of :cmd:`Require Export`.  If the module required has
+      already been loaded, :cmd:`Require Import` :n:`@qualid` simply imports it, as
+      :cmd:`Import` :n:`@qualid` would.
 
-This command acts as ``Require Import`` :n:`@qualid`,
-but if a further module, say `A`, contains a command ``Require Export`` `B`,
-then the command ``Require Import`` `A` also imports the module `B.`
+   .. cmdv:: Require Export @qualid
 
-.. cmdv:: Require [Import | Export] {+ @qualid }.
+      This command acts as ``Require Import`` :n:`@qualid`,
+      but if a further module, say `A`, contains a command ``Require Export`` `B`,
+      then the command ``Require Import`` `A` also imports the module `B.`
 
-This loads the
-modules named by the :n:`qualid` sequence and their recursive
-dependencies. If
-``Import`` or ``Export`` is given, it also imports these modules and
-all the recursive dependencies that were marked or transitively marked
-as ``Export``.
+   .. cmdv:: Require [Import | Export] {+ @qualid }
 
-.. cmdv:: From @dirpath Require @qualid.
+      This loads the
+      modules named by the :n:`qualid` sequence and their recursive
+      dependencies. If
+      ``Import`` or ``Export`` is given, it also imports these modules and
+      all the recursive dependencies that were marked or transitively marked
+      as ``Export``.
 
-This command acts as ``Require``, but picks
-any library whose absolute name is of the form dirpath.dirpath’.qualid
-for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library
-comes from a given package by making explicit its absolute root.
+   .. cmdv:: From @dirpath Require @qualid
 
+      This command acts as ``Require``, but picks
+      any library whose absolute name is of the form dirpath.dirpath’.qualid
+      for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library
+      comes from a given package by making explicit its absolute root.
 
+   .. exn:: Cannot load qualid: no physical path bound to dirpath.
 
-Error messages:
+   .. exn:: Cannot find library foo in loadpath.
 
-.. exn:: Cannot load qualid: no physical path bound to dirpath
+      The command did not find the
+      file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a
+      directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`).
 
-.. exn:: Cannot find library foo in loadpath
+   .. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid.
 
-The command did not find the
-file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a
-directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`).
+      The command tried to load library file :n:`@ident`.vo that
+      depends on some specific version of library :n:`@qualid` which is not the
+      one already loaded in the current |Coq| session. Probably `ident.v` was
+      not properly recompiled with the last version of the file containing
+      module :n:`@qualid`.
 
-.. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid
+   .. exn:: Bad magic number.
 
-The command tried to load library file :n:`@ident`.vo that
-depends on some specific version of library :n:`@qualid` which is not the
-one already loaded in the current |Coq| session. Probably `ident.v` was
-not properly recompiled with the last version of the file containing
-module :n:`@qualid`.
+      The file `ident.vo` was found but either it is not a
+      |Coq| compiled module, or it was compiled with an incompatible
+      version of |Coq|.
 
-.. exn:: Bad magic number
+   .. exn:: The file `ident.vo` contains library dirpath and not library dirpath’.
 
-The file `ident.vo` was found but either it is not a
-|Coq| compiled module, or it was compiled with an incompatible
-version of |Coq|.
+      The library file `dirpath’` is indirectly required by the
+      ``Require`` command but it is bound in the current loadpath to the
+      file `ident.vo` which was bound to a different library name `dirpath` at
+      the time it was compiled.
 
-.. exn:: The file `ident.vo` contains library dirpath and not library dirpath’
 
-The library file `dirpath’` is indirectly required by the
-``Require`` command but it is bound in the current loadpath to the
-file `ident.vo` which was bound to a different library name `dirpath` at
-the time it was compiled.
+   .. exn:: Require is not allowed inside a module or a module type.
 
-
-.. exn:: Require is not allowed inside a module or a module type
-
-This command
-is not allowed inside a module or a module type being defined. It is
-meant to describe a dependency between compilation units. Note however
-that the commands ``Import`` and ``Export`` alone can be used inside modules
-(see Section :ref:`Import <import_qualid>`).
+      This command
+      is not allowed inside a module or a module type being defined. It is
+      meant to describe a dependency between compilation units. Note however
+      that the commands ``Import`` and ``Export`` alone can be used inside modules
+      (see Section :ref:`Import <import_qualid>`).
 
 
 
 See also: Chapter :ref:`thecoqcommands`
 
 
-.. cmd:: Print Libraries.
-
-This command displays the list of library files loaded in the
-current |Coq| session. For each of these libraries, it also tells if it
-is imported.
-
-
-.. cmd:: Declare ML Module {+ @string } .
-
-This commands loads the OCaml compiled files
-with names given by the :n:`@string` sequence
-(dynamic link). It is mainly used to load tactics dynamically. The
-files are searched into the current OCaml loadpath (see the
-command ``Add ML Path`` in Section :ref:`libraries-and-filesystem`). Loading of OCaml files is only possible under the bytecode version of ``coqtop`` (i.e.
-``coqtop`` called with option ``-byte``, see chapter :ref:`thecoqcommands`), or when |Coq| has been compiled with a
-version of OCaml that supports native Dynlink (≥ 3.11).
-
-
-Variants:
-
+.. cmd:: Print Libraries
 
-.. cmdv:: Local Declare ML Module {+ @string }.
+   This command displays the list of library files loaded in the
+   current |Coq| session. For each of these libraries, it also tells if it
+   is imported.
 
-This variant is not
-exported to the modules that import the module where they occur, even
-if outside a section.
 
+.. cmd:: Declare ML Module {+ @string }
 
+   This commands loads the OCaml compiled files
+   with names given by the :n:`@string` sequence
+   (dynamic link). It is mainly used to load tactics dynamically. The
+   files are searched into the current OCaml loadpath (see the
+   command ``Add ML Path`` in Section :ref:`libraries-and-filesystem`).
+   Loading of OCaml files is only possible under the bytecode version of
+   ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter
+   :ref:`thecoqcommands`), or when |Coq| has been compiled with a
+   version of OCaml that supports native Dynlink (≥ 3.11).
 
-Error messages:
+   .. cmdv:: Local Declare ML Module {+ @string }
 
-.. exn:: File not found on loadpath : @string
+      This variant is not exported to the modules that import the module
+      where they occur, even if outside a section.
 
-.. exn:: Loading of ML object file forbidden in a native Coq
+   .. exn:: File not found on loadpath: @string.
 
+   .. exn:: Loading of ML object file forbidden in a native Coq.
 
 
-.. cmd:: Print ML Modules.
+.. cmd:: Print ML Modules
 
-This prints the name of all OCaml modules loaded with ``Declare
-ML Module``. To know from where these module were loaded, the user
-should use the command ``Locate File`` (see :ref:`here <locate-file>`)
+   This prints the name of all OCaml modules loaded with ``Declare
+   ML Module``. To know from where these module were loaded, the user
+   should use the command ``Locate File`` (see :ref:`here <locate-file>`)
 
 
 .. _loadpath:
@@ -811,110 +748,92 @@ for practical purposes. Such commands are only meant to be issued in
 the toplevel, and using them in source files is discouraged.
 
 
-.. cmd:: Pwd.
-
-This command displays the current working directory.
-
-
-.. cmd:: Cd @string.
-
-This command changes the current directory according to :n:`@string` which
-can be any valid path.
-
-
-Variants:
-
-
-.. cmdv:: Cd.
-
-Is equivalent to Pwd.
-
-
-
-.. cmd:: Add LoadPath @string as @dirpath.
-
-This command is equivalent to the command line option
-``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current
-|Coq| loadpath and maps it to the logical directory dirpath.
+.. cmd:: Pwd
 
-Variants:
+   This command displays the current working directory.
 
 
-.. cmdv:: Add LoadPath @string.
+.. cmd:: Cd @string
 
-Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but
-for the empty directory path.
+   This command changes the current directory according to :n:`@string` which
+   can be any valid path.
 
+   .. cmdv:: Cd
 
+      Is equivalent to Pwd.
 
-.. cmd:: Add Rec LoadPath @string as @dirpath.
 
-This command is equivalent to the command line option
-``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its
-subdirectories to the current |Coq| loadpath.
+.. cmd:: Add LoadPath @string as @dirpath
 
-Variants:
+   This command is equivalent to the command line option
+   ``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current
+   |Coq| loadpath and maps it to the logical directory dirpath.
 
+   .. cmdv:: Add LoadPath @string
 
-.. cmdv:: Add Rec LoadPath @string.
+      Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but
+      for the empty directory path.
 
-Works as ``Add Rec LoadPath`` :n:`@string` as :n:`@dirpath` but for the empty
-logical directory path.
 
+.. cmd:: Add Rec LoadPath @string as @dirpath
 
+   This command is equivalent to the command line option
+   ``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its
+   subdirectories to the current |Coq| loadpath.
 
-.. cmd:: Remove LoadPath @string.
+   .. cmdv:: Add Rec LoadPath @string
 
-This command removes the path :n:`@string` from the current |Coq| loadpath.
+      Works as :cmd:`Add Rec LoadPath` :n:`@string` as :n:`@dirpath` but for the empty
+      logical directory path.
 
 
-.. cmd:: Print LoadPath.
+.. cmd:: Remove LoadPath @string
 
-This command displays the current |Coq| loadpath.
+   This command removes the path :n:`@string` from the current |Coq| loadpath.
 
 
-Variants:
+.. cmd:: Print LoadPath
 
+   This command displays the current |Coq| loadpath.
 
-.. cmdv:: Print LoadPath @dirpath.
+   .. cmdv:: Print LoadPath @dirpath
 
-Works as ``Print LoadPath`` but displays only
-the paths that extend the :n:`@dirpath` prefix.
+      Works as :cmd:`Print LoadPath` but displays only
+      the paths that extend the :n:`@dirpath` prefix.
 
 
-.. cmd:: Add ML Path @string.
+.. cmd:: Add ML Path @string
 
-This command adds the path :n:`@string` to the current OCaml
-loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
+   This command adds the path :n:`@string` to the current OCaml
+   loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
 
 
-.. cmd:: Add Rec ML Path @string.
+.. cmd:: Add Rec ML Path @string
 
-This command adds the directory :n:`@string` and all its subdirectories to
-the current OCaml loadpath (see the command ``Declare ML Module``
-in Section :ref:`compiled-files`).
+   This command adds the directory :n:`@string` and all its subdirectories to
+   the current OCaml loadpath (see the command :cmd:`Declare ML Module`).
 
 
-.. cmd:: Print ML Path @string.
+.. cmd:: Print ML Path @string
 
-This command displays the current OCaml loadpath. This
-command makes sense only under the bytecode version of ``coqtop``, i.e.
-using option ``-byte``
-(see the command Declare ML Module in Section :ref:`compiled-files`).
+   This command displays the current OCaml loadpath. This
+   command makes sense only under the bytecode version of ``coqtop``, i.e.
+   using option ``-byte``
+   (see the command Declare ML Module in Section :ref:`compiled-files`).
 
 .. _locate-file:
 
-.. cmd:: Locate File @string.
+.. cmd:: Locate File @string
 
-This command displays the location of file string in the current
-loadpath. Typically, string is a .cmo or .vo or .v file.
+   This command displays the location of file string in the current
+   loadpath. Typically, string is a .cmo or .vo or .v file.
 
 
-.. cmd:: Locate Library @dirpath.
+.. cmd:: Locate Library @dirpath
 
-This command gives the status of the |Coq| module dirpath. It tells if
-the module is loaded and if not searches in the load path for a module
-of logical name :n:`@dirpath`.
+   This command gives the status of the |Coq| module dirpath. It tells if
+   the module is loaded and if not searches in the load path for a module
+   of logical name :n:`@dirpath`.
 
 
 .. _backtracking:
@@ -927,95 +846,71 @@ interactively, they cannot be part of a vernacular file loaded via
 ``Load`` or compiled by ``coqc``.
 
 
-.. cmd:: Reset @ident.
-
-This command removes all the objects in the environment since :n:`@ident`
-was introduced, including :n:`@ident`. :n:`@ident` may be the name of a defined or
-declared object as well as the name of a section. One cannot reset
-over the name of a module or of an object inside a module.
-
-
-Error messages:
-
-.. exn:: @ident: no such entry
-
-Variants:
-
-.. cmd:: Reset Initial.
-
-Goes back to the initial state, just after the start
-of the interactive session.
-
-
-
-.. cmd:: Back.
-
-This commands undoes all the effects of the last vernacular command.
-Commands read from a vernacular file via a ``Load`` are considered as a
-single command. Proof management commands are also handled by this
-command (see Chapter :ref:`proofhandling`). For that, Back may have to undo more than
-one command in order to reach a state where the proof management
-information is available. For instance, when the last command is a
-``Qed``, the management information about the closed proof has been
-discarded. In this case, ``Back`` will then undo all the proof steps up to
-the statement of this proof.
-
-
-Variants:
+.. cmd:: Reset @ident
 
+   This command removes all the objects in the environment since :n:`@ident`
+   was introduced, including :n:`@ident`. :n:`@ident` may be the name of a defined or
+   declared object as well as the name of a section. One cannot reset
+   over the name of a module or of an object inside a module.
 
-.. cmdv:: Back @num.
+   .. exn:: @ident: no such entry.
 
-Undoes :n:`@num` vernacular commands. As for Back, some extra
-commands may be undone in order to reach an adequate state. For
-instance Back :n:`@num` will not re-enter a closed proof, but rather go just
-before that proof.
+   .. cmdv:: Reset Initial
 
+      Goes back to the initial state, just after the start
+      of the interactive session.
 
 
-Error messages:
+.. cmd:: Back
 
+   This command undoes all the effects of the last vernacular command.
+   Commands read from a vernacular file via a :cmd:`Load` are considered as a
+   single command. Proof management commands are also handled by this
+   command (see Chapter :ref:`proofhandling`). For that, Back may have to undo more than
+   one command in order to reach a state where the proof management
+   information is available. For instance, when the last command is a
+   :cmd:`Qed`, the management information about the closed proof has been
+   discarded. In this case, :cmd:`Back` will then undo all the proof steps up to
+   the statement of this proof.
 
-.. exn:: Invalid backtrack
+   .. cmdv:: Back @num
 
-The user wants to undo more commands than available in the history.
+      Undo :n:`@num` vernacular commands. As for Back, some extra
+      commands may be undone in order to reach an adequate state. For
+      instance Back :n:`@num` will not re-enter a closed proof, but rather go just
+      before that proof.
 
-.. cmd:: BackTo @num.
+   .. exn:: Invalid backtrack.
 
-This command brings back the system to the state labeled :n:`@num`,
-forgetting the effect of all commands executed after this state. The
-state label is an integer which grows after each successful command.
-It is displayed in the prompt when in -emacs mode. Just as ``Back`` (see
-above), the ``BackTo`` command now handles proof states. For that, it may
-have to undo some extra commands and end on a state `num′ ≤ num` if
-necessary.
+      The user wants to undo more commands than available in the history.
 
+.. cmd:: BackTo @num
 
-Variants:
+   This command brings back the system to the state labeled :n:`@num`,
+   forgetting the effect of all commands executed after this state. The
+   state label is an integer which grows after each successful command.
+   It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see
+   above), the :cmd:`BackTo` command now handles proof states. For that, it may
+   have to undo some extra commands and end on a state `num′ ≤ num` if
+   necessary.
 
+   .. cmdv:: Backtrack @num @num @num
 
-.. cmdv:: Backtrack @num @num @num.
+      .. deprecated:: 8.4
 
-`Backtrack` is a *deprecated* form of
-`BackTo` which allows explicitly manipulating the proof environment. The
-three numbers represent the following:
+      :cmd:`Backtrack` is a *deprecated* form of
+      :cmd:`BackTo` which allows explicitly manipulating the proof environment. The
+      three numbers represent the following:
 
-    + *first number* : State label to reach, as for BackTo.
-    + *second number* : *Proof state number* to unbury once aborts have been done.
-      |Coq| will compute the number of Undo to perform (see Chapter :ref:`proofhandling`).
-    + *third number* : Number of Abort to perform, i.e. the number of currently
-      opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`).
+      + *first number* : State label to reach, as for :cmd:`BackTo`.
+      + *second number* : *Proof state number* to unbury once aborts have been done.
+        |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`).
+      + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently
+        opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`).
 
+   .. exn:: Invalid backtrack.
 
-
-
-Error messages:
-
-
-.. exn:: Invalid backtrack
-
-
-The destination state label is unknown.
+      The destination state label is unknown.
 
 
 .. _quitting-and-debugging:
@@ -1024,86 +919,81 @@ Quitting and debugging
 --------------------------
 
 
-.. cmd:: Quit.
-
-This command permits to quit |Coq|.
+.. cmd:: Quit
 
+   This command permits to quit |Coq|.
 
-.. cmd:: Drop.
 
-This is used mostly as a debug facility by |Coq|’s implementors and does
-not concern the casual user. This command permits to leave |Coq|
-temporarily and enter the OCaml toplevel. The OCaml
-command:
+.. cmd:: Drop
 
+   This is used mostly as a debug facility by |Coq|’s implementors and does
+   not concern the casual user. This command permits to leave |Coq|
+   temporarily and enter the OCaml toplevel. The OCaml
+   command:
 
-::
+   ::
 
-    #use "include";;
+      #use "include";;
 
+   adds the right loadpaths and loads some toplevel printers for all
+   abstract types of |Coq|- section_path, identifiers, terms, judgments, ….
+   You can also use the file base_include instead, that loads only the
+   pretty-printers for section_paths and identifiers. You can return back
+   to |Coq| with the command:
 
-adds the right loadpaths and loads some toplevel printers for all
-abstract types of |Coq|- section_path, identifiers, terms, judgments, ….
-You can also use the file base_include instead, that loads only the
-pretty-printers for section_paths and identifiers. You can return back
-to |Coq| with the command:
+   ::
 
+      go();;
 
-::
-
-    go();;
-
-.. warning::
-
-   #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`,
-      see Section `interactive-use`).
-   #. You must have compiled |Coq| from the source package and set the
-      environment variable COQTOP to the root of your copy of the sources
-      (see Section `customization-by-environment-variables`).
+   .. warning::
 
+      #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`,
+         see Section `interactive-use`).
+      #. You must have compiled |Coq| from the source package and set the
+         environment variable COQTOP to the root of your copy of the sources
+         (see Section `customization-by-environment-variables`).
 
 
 .. TODO : command is not a syntax entry
 
-.. cmd:: Time @command.
+.. cmd:: Time @command
 
-This command executes the vernacular command :n:`@command` and displays the
-time needed to execute it.
+   This command executes the vernacular command :n:`@command` and displays the
+   time needed to execute it.
 
 
-.. cmd:: Redirect @string @command.
+.. cmd:: Redirect @string @command
 
-This command executes the vernacular command :n:`@command`, redirecting its
-output to ":n:`@string`.out".
+   This command executes the vernacular command :n:`@command`, redirecting its
+   output to ":n:`@string`.out".
 
 
-.. cmd:: Timeout @num @command.
+.. cmd:: Timeout @num @command
 
-This command executes the vernacular command :n:`@command`. If the command
-has not terminated after the time specified by the :n:`@num` (time
-expressed in seconds), then it is interrupted and an error message is
-displayed.
+   This command executes the vernacular command :n:`@command`. If the command
+   has not terminated after the time specified by the :n:`@num` (time
+   expressed in seconds), then it is interrupted and an error message is
+   displayed.
 
+   .. opt:: Default Timeout @num
 
-.. opt:: Default Timeout @num
+      This option controls a default timeout for subsequent commands, as if they
+      were passed to a :cmd:`Timeout` command. Commands already starting by a
+      :cmd:`Timeout` are unaffected.
 
-   This option controls a default timeout for subsequent commands, as if they
-   were passed to a :cmd:`Timeout` command. Commands already starting by a
-   :cmd:`Timeout` are unaffected.
 
-.. cmd:: Fail @command.
+.. cmd:: Fail @command
 
-For debugging scripts, sometimes it is desirable to know
-whether a command or a tactic fails. If the given :n:`@command`
-fails, the ``Fail`` statement succeeds, without changing the proof
-state, and in interactive mode, the system
-prints a message confirming the failure.
-If the given :n:`@command` succeeds, the statement is an error, and
-it prints a message indicating that the failure did not occur.
+   For debugging scripts, sometimes it is desirable to know
+   whether a command or a tactic fails. If the given :n:`@command`
+   fails, the ``Fail`` statement succeeds, without changing the proof
+   state, and in interactive mode, the system
+   prints a message confirming the failure.
+   If the given :n:`@command` succeeds, the statement is an error, and
+   it prints a message indicating that the failure did not occur.
 
-Error messages:
+   .. exn:: The command has not failed!
 
-.. exn:: The command has not failed!
 
 .. _controlling-display:
 
@@ -1131,13 +1021,13 @@ Controlling display
    :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their
    output, printing only identifiers.
 
-.. opt:: Printing Width @integer
+.. opt:: Printing Width @num
 
    This command sets which left-aligned part of the width of the screen is used
    for display. At the time of writing this documentation, the default value
    is 78.
 
-.. opt:: Printing Depth @integer
+.. opt:: Printing Depth @num
 
    This option controls the nesting depth of the formatter used for pretty-
    printing. Beyond this depth, display of subterms is replaced by dots. At the
@@ -1181,79 +1071,77 @@ as numbers, and for reflection-based tactics. The commands to fine-
 tune the reduction strategies and the lazy conversion algorithm are
 described first.
 
-.. cmd:: Opaque {+ @qualid }.
-
-This command has an effect on unfoldable constants, i.e. on constants
-defined by ``Definition`` or ``Let`` (with an explicit body), or by a command
-assimilated to a definition such as ``Fixpoint``, ``Program Definition``, etc,
-or by a proof ended by ``Defined``. The command tells not to unfold the
-constants in the :n:`@qualid` sequence in tactics using δ-conversion (unfolding
-a constant is replacing it by its definition).
-
-``Opaque`` has also an effect on the conversion algorithm of |Coq|, telling
-it to delay the unfolding of a constant as much as possible when |Coq|
-has to check the conversion (see Section :ref:`conversion-rules`) of two distinct
-applied constants.
-
-The scope of ``Opaque`` is limited to the current section, or current
-file, unless the variant ``Global Opaque`` is used.
+.. cmd:: Opaque {+ @qualid }
 
+   This command has an effect on unfoldable constants, i.e. on constants
+   defined by :cmd:`Definition` or :cmd:`Let` (with an explicit body), or by a command
+   assimilated to a definition such as :cmd:`Fixpoint`, :cmd:`Program Definition`, etc,
+   or by a proof ended by :cmd:`Defined`. The command tells not to unfold the
+   constants in the :n:`@qualid` sequence in tactics using δ-conversion (unfolding
+   a constant is replacing it by its definition).
 
-See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
+   :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling
+   it to delay the unfolding of a constant as much as possible when |Coq|
+   has to check the conversion (see Section :ref:`conversion-rules`) of two distinct
+   applied constants.
 
+   .. cmdv:: Global Opaque {+ @qualid }
+      :name: Global Opaque
 
-Error messages:
+      The scope of :cmd:`Opaque` is limited to the current section, or current
+      file, unless the variant :cmd:`Global Opaque` is used.
 
+   See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`,
+   :ref:`proof-editing-mode`
 
-.. exn:: The reference @qualid was not found in the current environment
+   .. exn:: The reference @qualid was not found in the current environment.
 
-There is no constant referred by :n:`@qualid` in the environment.
-Nevertheless, if you asked ``Opaque`` `foo` `bar` and if `bar` does not exist, `foo` is set opaque.
+      There is no constant referred by :n:`@qualid` in the environment.
+      Nevertheless, if you asked :cmd:`Opaque` `foo` `bar` and if `bar` does
+      not exist, `foo` is set opaque.
 
-.. cmd:: Transparent {+ @qualid }.
+.. cmd:: Transparent {+ @qualid }
 
-This command is the converse of `Opaque`` and it applies on unfoldable
-constants to restore their unfoldability after an Opaque command.
+   This command is the converse of :cmd:`Opaque` and it applies on unfoldable
+   constants to restore their unfoldability after an Opaque command.
 
-Note in particular that constants defined by a proof ended by Qed are
-not unfoldable and Transparent has no effect on them. This is to keep
-with the usual mathematical practice of *proof irrelevance*: what
-matters in a mathematical development is the sequence of lemma
-statements, not their actual proofs. This distinguishes lemmas from
-the usual defined constants, whose actual values are of course
-relevant in general.
+   Note in particular that constants defined by a proof ended by Qed are
+   not unfoldable and Transparent has no effect on them. This is to keep
+   with the usual mathematical practice of *proof irrelevance*: what
+   matters in a mathematical development is the sequence of lemma
+   statements, not their actual proofs. This distinguishes lemmas from
+   the usual defined constants, whose actual values are of course
+   relevant in general.
 
-The scope of Transparent is limited to the current section, or current
-file, unless the variant ``Global Transparent`` is
-used.
+   .. cmdv:: Global Transparent {+ @qualid }
+      :name: Global Transparent
 
+      The scope of Transparent is limited to the current section, or current
+      file, unless the variant :cmd:`Global Transparent` is
+      used.
 
-Error messages:
+   .. exn:: The reference @qualid was not found in the current environment.
 
+      There is no constant referred by :n:`@qualid` in the environment.
 
-.. exn:: The reference @qualid was not found in the current environment
-
-There is no constant referred by :n:`@qualid` in the environment.
-
-
-
-See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
+   See also: sections :ref:`performingcomputations`,
+   :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
 
 .. _vernac-strategy:
 
-.. cmd:: Strategy @level [ {+ @qualid } ].
+.. cmd:: Strategy @level [ {+ @qualid } ]
 
-This command generalizes the behavior of Opaque and Transparent
-commands. It is used to fine-tune the strategy for unfolding
-constants, both at the tactic level and at the kernel level. This
-command associates a level to the qualified names in the :n:`@qualid`
-sequence. Whenever two
-expressions with two distinct head constants are compared (for
-instance, this comparison can be triggered by a type cast), the one
-with lower level is expanded first. In case of a tie, the second one
-(appearing in the cast type) is expanded.
+   This command generalizes the behavior of Opaque and Transparent
+   commands. It is used to fine-tune the strategy for unfolding
+   constants, both at the tactic level and at the kernel level. This
+   command associates a level to the qualified names in the :n:`@qualid`
+   sequence. Whenever two
+   expressions with two distinct head constants are compared (for
+   instance, this comparison can be triggered by a type cast), the one
+   with lower level is expanded first. In case of a tie, the second one
+   (appearing in the cast type) is expanded.
 
-Levels can be one of the following (higher to lower):
+   Levels can be one of the following (higher to lower):
 
     + ``opaque`` : level of opaque constants. They cannot be expanded by
       tactics (behaves like +∞, see next item).
@@ -1266,52 +1154,42 @@ Levels can be one of the following (higher to lower):
     + ``expand`` : level of constants that should be expanded first (behaves
       like −∞)
 
+    .. cmdv:: Local Strategy @level [ {+ @qualid } ]
 
-These directives survive section and module closure, unless the
-command is prefixed by Local. In the latter case, the behavior
-regarding sections and modules is the same as for the ``Transparent`` and
-``Opaque`` commands.
-
-
-.. cmd:: Print Strategy @qualid.
-
-This command prints the strategy currently associated to :n:`@qualid`. It
-fails if :n:`@qualid` is not an unfoldable reference, that is, neither a
-variable nor a constant.
-
-
-Error messages:
-
-
-.. exn:: The reference is not unfoldable.
-
-
+       These directives survive section and module closure, unless the
+       command is prefixed by ``Local``. In the latter case, the behavior
+       regarding sections and modules is the same as for the :cmd:`Transparent` and
+       :cmd:`Opaque` commands.
 
-Variants:
 
+.. cmd:: Print Strategy @qualid
 
-.. cmdv:: Print Strategies.
+   This command prints the strategy currently associated to :n:`@qualid`. It
+   fails if :n:`@qualid` is not an unfoldable reference, that is, neither a
+   variable nor a constant.
 
-Print all the currently non-transparent strategies.
+   .. exn:: The reference is not unfoldable.
 
+   .. cmdv:: Print Strategies
 
+      Print all the currently non-transparent strategies.
 
-.. cmd:: Declare Reduction @ident := @convtactic.
 
-This command allows giving a short name to a reduction expression, for
-instance lazy beta delta [foo bar]. This short name can then be used
-in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command
-accepts the
-Local modifier, for discarding this reduction name at the end of the
-file or module. For the moment the name cannot be qualified. In
-particular declaring the same name in several modules or in several
-functor applications will be refused if these declarations are not
-local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but
-nothing prevents the user to also perform a
-``Ltac`` `ident` ``:=`` `convtactic`.
+.. cmd:: Declare Reduction @ident := @convtactic
 
+   This command allows giving a short name to a reduction expression, for
+   instance lazy beta delta [foo bar]. This short name can then be used
+   in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command
+   accepts the
+   Local modifier, for discarding this reduction name at the end of the
+   file or module. For the moment the name cannot be qualified. In
+   particular declaring the same name in several modules or in several
+   functor applications will be refused if these declarations are not
+   local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but
+   nothing prevents the user to also perform a
+   ``Ltac`` `ident` ``:=`` `convtactic`.
 
-See also: sections :ref:`performingcomputations`
+   See also: sections :ref:`performingcomputations`
 
 
 .. _controlling-locality-of-commands:
@@ -1320,8 +1198,8 @@ Controlling the locality of commands
 -----------------------------------------
 
 
-.. cmd:: Local @command.
-.. cmd:: Global @command.
+.. cmd:: Local @command
+.. cmd:: Global @command
 
 Some commands support a Local or Global prefix modifier to control the
 scope of their effect. There are four kinds of commands: