Merge PR #9036: Add bodies to sphinx objects.

4 files changed, 474 insertions, 402 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index edd83b7cee..0ea8c7be2d 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -292,6 +292,7 @@ focused goals with:
 
    .. exn:: No such goal.
       :name: No such goal. (Goal selector)
+      :undocumented:
 
    .. TODO change error message index entry
 
@@ -351,6 +352,7 @@ We can check if a tactic made progress with:
    goals (up to syntactical equality), then an error of level 0 is raised.
 
    .. exn:: Failed to progress.
+      :undocumented:
 
 Backtracking branching
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -393,6 +395,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics:
    :n:`v__i` to have *at least* one success.
 
    .. exn:: No applicable tactic.
+      :undocumented:
 
    .. tacv:: first @expr
 
@@ -482,6 +485,7 @@ one* success:
       immediately.
 
    .. exn:: This tactic has more than one success.
+      :undocumented:
 
 Checking the failure
 ~~~~~~~~~~~~~~~~~~~~
@@ -521,6 +525,7 @@ among a panel of tactics:
    apply :n:`v__2` and so on. It fails if there is no solving tactic.
 
    .. exn:: Cannot solve the goal.
+      :undocumented:
 
    .. tacv:: solve @expr
 
@@ -576,8 +581,7 @@ Failing
       goals left. See the example for clarification.
 
    .. tacv:: gfail {* message_token}
-
-   .. tacv:: gfail @num {* message_token}
+             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
@@ -586,9 +590,11 @@ Failing
       evaluated, a tactic call like :n:`let x := H in fail 0 x` will succeed.
 
    .. exn:: Tactic Failure message (level @num).
+      :undocumented:
 
    .. exn:: No such goal.
       :name: No such goal. (fail)
+      :undocumented:
 
    .. example::
 
@@ -670,24 +676,24 @@ tactic
 
    This tactic currently does not support nesting, and will report times
    based on the innermost execution. This is due to the fact that it is
-   implemented using the tactics
+   implemented using the following internal tactics:
 
    .. tacn:: restart_timer @string
       :name: restart_timer
 
-   and
+      Reset a timer
 
-   .. tacn:: finish_timing {? @string} @string
+   .. tacn:: finish_timing {? (@string)} @string
       :name: finish_timing
 
-   which (re)set and display an optionally named timer, respectively. The
-   parenthesized string argument to :n:`finish_timing` is also optional, and
-   determines the label associated with the timer for printing.
+      Display an optionally named timer. The parenthesized string argument
+      is also optional, and determines the label associated with the timer
+      for printing.
 
-   By copying the definition of :n:`time_constr` from the standard library,
+   By copying the definition of :tacn:`time_constr` from the standard library,
    users can achive support for a fixed pattern of nesting by passing
-   different :n:`@string` parameters to :n:`restart_timer` and :n:`finish_timing`
-   at each level of nesting.
+   different :token:`string` parameters to :tacn:`restart_timer` and
+   :tacn:`finish_timing` at each level of nesting.
 
    .. example::
 
@@ -967,10 +973,10 @@ Evaluation of a term can be performed with:
 Recovering the type of a term
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The following returns the type of term:
-
 .. tacn:: type of @term
 
+   This tactic returns the type of :token:`term`.
+
 Manipulating untyped terms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1041,6 +1047,7 @@ Testing boolean expressions
          Fail all:let n:= numgoals in guard n=2.
 
    .. exn:: Condition not satisfied.
+      :undocumented:
 
 Proving a subgoal as a separate lemma
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1092,6 +1099,7 @@ Proving a subgoal as a separate lemma
 
    .. exn:: Proof is not complete.
       :name: Proof is not complete. (abstract)
+      :undocumented:
 
 Tactic toplevel definitions
 ---------------------------
@@ -1348,6 +1356,6 @@ Run-time optimization tactic
 .. tacn:: optimize_heap
    :name: optimize_heap
 
-This tactic behaves like :n:`idtac`, except that running it compacts the
-heap in the OCaml run-time system. It is analogous to the Vernacular
-command :cmd:`Optimize Heap`.
+   This tactic behaves like :n:`idtac`, except that running it compacts the
+   heap in the OCaml run-time system. It is analogous to the Vernacular
+   command :cmd:`Optimize Heap`.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 0b059f92ee..590d71b5f3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -67,6 +67,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
    added to the environment as an opaque constant.
 
    .. exn:: Attempt to save an incomplete proof.
+      :undocumented:
 
    .. note::
 
@@ -106,6 +107,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
    proof was edited.
 
    .. exn:: No focused proof (No proof-editing in progress).
+      :undocumented:
 
    .. cmdv::  Abort @ident
 
@@ -282,6 +284,7 @@ Navigation in the proof tree
    This command restores the proof editing process to the original goal.
 
    .. exn:: No focused proof to restart.
+      :undocumented:
 
 .. cmd:: Focus
 
@@ -473,13 +476,14 @@ Requesting information
    This command displays the current goals.
 
    .. exn:: No focused proof.
+      :undocumented:
 
    .. cmdv:: Show @num
 
       Displays only the :token:`num`\-th subgoal.
 
       .. exn:: No such goal.
-
+         :undocumented:
 
    .. cmdv:: Show @ident
 
@@ -565,6 +569,7 @@ Requesting information
             Show Match nat.
 
       .. exn:: Unknown inductive type.
+         :undocumented:
 
    .. cmdv:: Show Universes
       :name: Show Universes
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 041f1bc966..150aadc15a 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -91,6 +91,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
   of ``term``.
 
   .. exn:: No such binder.
+     :undocumented:
 
 + A bindings list can also be a simple list of terms :n:`{* term}`.
   In that case the references to which these terms correspond are
@@ -102,6 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
   are required.
 
   .. exn:: Not the right number of missing arguments.
+     :undocumented:
 
 .. _occurrencessets:
 
@@ -589,6 +591,7 @@ Applying theorems
       :n:`constructor 2 {? with @bindings_list }`.
 
       .. exn:: Not an inductive goal with 2 constructors.
+         :undocumented:
 
    .. tacv:: econstructor
              eexists
@@ -1081,8 +1084,8 @@ Managing the local context
       generated by Coq.
 
    .. tacv:: epose (@ident {? @binders} := @term)
-   .. tacv:: epose term
-      :name: epose
+             epose @term
+      :name: epose; _
 
       While the different variants of :tacn:`pose` expect that no
       existential variables are generated by the tactic, :tacn:`epose`
@@ -1124,7 +1127,7 @@ Managing the local context
 Controlling the proof flow
 ------------------------------
 
-.. tacn:: assert (@ident : form)
+.. tacn:: assert (@ident : @type)
    :name: assert
 
    This tactic applies to any goal. :n:`assert (H : U)` adds a new hypothesis
@@ -1132,106 +1135,104 @@ 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`.
+      Arises when the argument :token:`type` is neither of type :g:`Prop`,
+      :g:`Set` nor :g:`Type`.
 
-.. tacv:: assert form
+   .. tacv:: assert @type
 
-   This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by
-   Coq.
+      This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is
+      generated by Coq.
 
-.. tacv:: assert @form by @tactic
+   .. tacv:: assert @type by @tactic
 
-   This tactic behaves like :n:`assert` but applies tactic to solve the subgoals
-   generated by assert.
+      This tactic behaves like :tacn:`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)
+         :undocumented:
 
-.. tacv:: assert @form as @intro_pattern
+   .. tacv:: assert @type as @intro_pattern
 
-   If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`),
-   the hypothesis is named after this introduction pattern (in particular, if
-   :n:`intro_pattern` is :n:`@ident`, the tactic behaves like
-   :n:`assert (@ident : form)`). If :n:`intro_pattern` is an action
-   introduction pattern, the tactic behaves like :n:`assert form` followed by
-   the action done by this introduction pattern.
+      If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`),
+      the hypothesis is named after this introduction pattern (in particular, if
+      :n:`intro_pattern` is :n:`@ident`, the tactic behaves like
+      :n:`assert (@ident : @type)`). If :n:`intro_pattern` is an action
+      introduction pattern, the tactic behaves like :n:`assert @type` followed by
+      the action done by this introduction pattern.
 
-.. tacv:: assert @form as @intro_pattern by @tactic
+   .. tacv:: assert @type as @intro_pattern by @tactic
 
-   This combines the two previous variants of :n:`assert`.
+      This combines the two previous variants of :tacn:`assert`.
 
-.. tacv:: assert (@ident := @term )
+   .. tacv:: assert (@ident := @term)
 
-   This behaves as :n:`assert (@ident : type) by exact @term` where :g:`type` is
-   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`.
+      This behaves as :n:`assert (@ident : @type) by exact @term` where
+      :token:`type` is the type of :token:`term`. This is equivalent to using
+      :tacn:`pose proof`. If the head of term is :token:`ident`, the tactic
+      behaves as :tacn:`specialize`.
 
-   .. exn:: Variable @ident is already declared.
+      .. exn:: Variable @ident is already declared.
+         :undocumented:
 
-.. tacv:: eassert form as intro_pattern by tactic
+.. tacv:: eassert @type as @intro_pattern by @tactic
    :name: eassert
 
-.. tacv:: assert (@ident := @term)
-
-   While the different variants of :n:`assert` expect that no existential
-   variables are generated by the tactic, :n:`eassert` removes this constraint.
+   While the different variants of :tacn:`assert` expect that no existential
+   variables are generated by the tactic, :tacn:`eassert` removes this constraint.
    This allows not to specify the asserted statement completeley before starting
    to prove it.
 
-.. tacv:: pose proof @term {? as intro_pattern}
+.. tacv:: pose proof @term {? as @intro_pattern}
    :name: pose proof
 
-   This tactic behaves like :n:`assert T {? as intro_pattern} by exact @term`
-   where :g:`T` is the type of :g:`term`. In particular,
+   This tactic behaves like :n:`assert @type {? as @intro_pattern} by exact @term`
+   where :token:`type` is the type of :token:`term`. In particular,
    :n:`pose proof @term as @ident` behaves as :n:`assert (@ident := @term)`
-   and :n:`pose proof @term as intro_pattern` is the same as applying the
-   intro_pattern to :n:`@term`.
+   and :n:`pose proof @term as @intro_pattern` is the same as applying the
+   :token:`intro_pattern` to :token:`term`.
 
-.. tacv:: epose proof term {? as intro_pattern}
+.. tacv:: epose proof @term {? as @intro_pattern}
+   :name: epose proof
 
-   While :n:`pose proof` expects that no existential variables are generated by
-   the tactic, :n:`epose proof` removes this constraint.
+   While :tacn:`pose proof` expects that no existential variables are generated by
+   the tactic, :tacn:`epose proof` removes this constraint.
 
-.. tacv:: enough (@ident : form)
+.. tacv:: enough (@ident : @type)
    :name: enough
 
-   This adds a new hypothesis of name :n:`@ident` asserting :n:`form` to the
-   goal the tactic :n:`enough` is applied to. A new subgoal stating :n:`form` is
-   inserted after the initial goal rather than before it as :n:`assert` would do.
+   This adds a new hypothesis of name :token:`ident` asserting :token:`type` to the
+   goal the tactic :tacn:`enough` is applied to. A new subgoal stating :token:`type` is
+   inserted after the initial goal rather than before it as :tacn:`assert` would do.
 
-.. tacv:: enough form
+.. tacv:: enough @type
 
-   This behaves like :n:`enough (@ident : form)` with the name :n:`@ident` of
+   This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of
    the hypothesis generated by Coq.
 
-.. tacv:: enough form as intro_pattern
+.. tacv:: enough @type as @intro_pattern
 
-   This behaves like :n:`enough form` using :n:`intro_pattern` to name or
+   This behaves like :n:`enough @type` using :token:`intro_pattern` to name or
    destruct the new hypothesis.
 
-.. tacv:: enough (@ident : @form) by @tactic
-.. tacv:: enough @form by @tactic
-.. tacv:: enough @form as @intro_pattern by @tactic
+.. tacv:: enough (@ident : @type) by @tactic
+          enough @type {? as @intro_pattern } by @tactic
 
-   This behaves as above but with :n:`tactic` expected to solve the initial goal
-   after the extra assumption :n:`form` is added and possibly destructed. If the
-   :n:`as intro_pattern` clause generates more than one subgoal, :n:`tactic` is
+   This behaves as above but with :token:`tactic` expected to solve the initial goal
+   after the extra assumption :token:`type` is added and possibly destructed. If the
+   :n:`as @intro_pattern` clause generates more than one subgoal, :token:`tactic` is
    applied to all of them.
 
-.. tacv:: eenough (@ident : form) by tactic
-   :name: eenough
-
-.. tacv:: eenough form by tactic
+.. tacv:: eenough @type {? as @intro_pattern } {? by @tactic }
+          eenough (@ident : @type) {? by @tactic }
+   :name: eenough; _
 
-.. tacv:: eenough form as intro_pattern by tactic
+   While the different variants of :tacn:`enough` expect that no existential
+   variables are generated by the tactic, :tacn:`eenough` removes this constraint.
 
-   While the different variants of :n:`enough` expect that no existential
-   variables are generated by the tactic, :n:`eenough` removes this constraint.
-
-.. tacv:: cut @form
+.. tacv:: cut @type
    :name: cut
 
    This tactic applies to any goal. It implements the non-dependent case of
@@ -1240,11 +1241,11 @@ Controlling the proof flow
    subgoals: :g:`U -> T` and :g:`U`. The subgoal :g:`U -> T` comes first in the
    list of remaining subgoal to prove.
 
-.. tacv:: specialize (ident {* @term}) {? as intro_pattern}
-.. tacv:: specialize ident with @bindings_list {? as intro_pattern}
-   :name: specialize
+.. tacv:: specialize (@ident {* @term}) {? as @intro_pattern}
+          specialize @ident with @bindings_list {? as @intro_pattern}
+   :name: specialize; _
 
-   The tactic :n:`specialize` works on local hypothesis :n:`@ident`. The
+   This tactic works on local hypothesis :n:`@ident`. The
    premises of this hypothesis (either universal quantifications or
    non-dependent implications) are instantiated by concrete terms coming either
    from arguments :n:`{* @term}` or from a :ref:`bindings list <bindingslist>`.
@@ -1254,15 +1255,18 @@ Controlling the proof flow
    uninstantiated arguments are inferred by unification if possible or left
    quantified in the hypothesis otherwise. With the :n:`as` clause, the local
    hypothesis :n:`@ident` is left unchanged and instead, the modified hypothesis
-   is introduced as specified by the :n:`intro_pattern`. The name :n:`@ident`
+   is introduced as specified by the :token:`intro_pattern`. The name :n:`@ident`
    can also refer to a global lemma or hypothesis. In this case, for
-   compatibility reasons, the behavior of :n:`specialize` is close to that of
-   :n:`generalize`: the instantiated statement becomes an additional premise of
-   the goal. The :n:`as` clause is especially useful in this case to immediately
+   compatibility reasons, the behavior of :tacn:`specialize` is close to that of
+   :tacn:`generalize`: the instantiated statement becomes an additional premise of
+   the goal. The ``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.
+      :undocumented:
+
    .. exn:: @ident is used in conclusion.
+      :undocumented:
 
 .. tacn:: generalize @term
    :name: generalize
@@ -1343,8 +1347,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
    changes in the goal, its use is strongly discouraged.
 
 .. tacv:: instantiate ( @num := @term ) in @ident
-.. tacv:: instantiate ( @num := @term ) in ( value of @ident )
-.. tacv:: instantiate ( @num := @term ) in ( type of @ident )
+          instantiate ( @num := @term ) in ( value of @ident )
+          instantiate ( @num := @term ) in ( type of @ident )
 
    These allow to refer respectively to existential variables occurring in a
    hypothesis or in the body or the type of a local definition.
@@ -1360,13 +1364,13 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
 .. tacn:: admit
    :name: admit
 
-The admit tactic allows temporarily skipping a subgoal so as to
-progress further in the rest of the proof. A proof containing admitted
-goals cannot be closed with :g:`Qed` but only with :g:`Admitted`.
+   This tactic allows temporarily skipping a subgoal so as to
+   progress further in the rest of the proof. A proof containing admitted
+   goals cannot be closed with :cmd:`Qed` but only with :cmd:`Admitted`.
 
 .. tacv:: give_up
 
-   Synonym of :n:`admit`.
+   Synonym of :tacn:`admit`.
 
 .. tacn:: absurd @term
    :name: absurd
@@ -1387,7 +1391,8 @@ 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.
+      :undocumented:
 
 .. tacv:: contradiction @ident
 
@@ -1602,6 +1607,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       induction n.
 
 .. exn:: Not an inductive product.
+   :undocumented:
 
 .. exn:: Unable to find an instance for the variables @ident ... @ident.
 
@@ -1672,10 +1678,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
          Show 2.
 
 .. tacv:: induction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences
+          einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences
 
-.. tacv:: einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences
-
-   These are the most general forms of ``induction`` and ``einduction``. It combines the
+   These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the
    effects of the with, as, using, and in clauses.
 
 .. tacv:: elim @term
@@ -1709,7 +1714,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    existential variables to be resolved later on.
 
 .. tacv:: elim @term using @term
-.. tacv:: elim @term using @term with @bindings_list
+          elim @term using @term with @bindings_list
 
    Allows the user to give explicitly an induction principle :n:`@term` that
    is not the standard one for the underlying inductive type of :n:`@term`. The
@@ -1717,15 +1722,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    :n:`@term`.
 
 .. tacv:: elim @term with @bindings_list using @term with @bindings_list
-.. tacv:: eelim @term with @bindings_list using @term with @bindings_list
+          eelim @term with @bindings_list using @term with @bindings_list
 
-   These are the most general forms of ``elim`` and ``eelim``. It combines the
+   These are the most general forms of :tacn:`elim` and :tacn:`eelim`. It combines the
    effects of the ``using`` clause and of the two uses of the ``with`` clause.
 
-.. tacv:: elimtype @form
+.. tacv:: elimtype @type
    :name: elimtype
 
-   The argument :n:`form` must be inductively defined. :n:`elimtype I` is
+   The argument :token:`type` must be inductively defined. :n:`elimtype I` is
    equivalent to :n:`cut I. intro Hn; elim Hn; clear Hn.` Therefore the
    hypothesis :g:`Hn` will not appear in the context(s) of the subgoal(s).
    Conversely, if :g:`t` is a :n:`@term` of (inductive) type :g:`I` that does
@@ -1879,7 +1884,10 @@ and an explanation of the underlying technique.
 .. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion`
 
 .. exn:: Cannot find induction information on @qualid.
+   :undocumented:
+
 .. exn:: Not the right number of induction arguments.
+   :undocumented:
 
 .. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list
 
@@ -1913,7 +1921,10 @@ and an explanation of the underlying technique.
    :n:`intros until @ident`.
 
 .. exn:: No primitive equality found.
+   :undocumented:
+
 .. exn:: Not a discriminable equality.
+   :undocumented:
 
 .. tacv:: discriminate @num
 
@@ -1927,11 +1938,11 @@ and an explanation of the underlying technique.
    bindings to instantiate parameters or hypotheses of :n:`@term`.
 
 .. tacv:: ediscriminate @num
-.. tacv:: ediscriminate @term {? with @bindings_list}
-   :name: ediscriminate
+          ediscriminate @term {? with @bindings_list}
+   :name: ediscriminate; _
 
-   This works the same as ``discriminate`` but if the type of :n:`@term`, or the
-   type of the hypothesis referred to by :n:`@num`, has uninstantiated
+   This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the
+   type of the hypothesis referred to by :token:`num`, has uninstantiated
    parameters, these parameters are left as existential variables.
 
 .. tacv:: discriminate
@@ -1942,6 +1953,7 @@ and an explanation of the underlying technique.
    :n:`intro @ident; discriminate @ident`.
 
    .. exn:: No discriminable equalities.
+      :undocumented:
 
 .. tacn:: injection @term
    :name: injection
@@ -1994,9 +2006,16 @@ and an explanation of the underlying technique.
       context using :n:`intros until @ident`.
 
    .. exn:: Not a projectable equality but a discriminable one.
-   .. exn:: Nothing to do, it is an equality between convertible @terms.
+      :undocumented:
+
+   .. exn:: Nothing to do, it is an equality between convertible terms.
+      :undocumented:
+
    .. exn:: Not a primitive equality.
+      :undocumented:
+
    .. exn:: Nothing to inject.
+      :undocumented:
 
    .. tacv:: injection @num
 
@@ -2010,8 +2029,8 @@ and an explanation of the underlying technique.
       instantiate parameters or hypotheses of :n:`@term`.
 
    .. tacv:: einjection @num
-      :name: einjection
-   .. tacv:: einjection @term {? with @bindings_list}
+             einjection @term {? with @bindings_list}
+      :name: einjection; _
 
       This works the same as :n:`injection` but if the type of :n:`@term`, or the
       type of the hypothesis referred to by :n:`@num`, has uninstantiated
@@ -2023,21 +2042,22 @@ and an explanation of the underlying technique.
       :n:`intro @ident; injection @ident`.
 
       .. exn:: goal does not satisfy the expected preconditions.
+         :undocumented:
 
    .. 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
-   :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 a hypothesis.
+             injection @num as {+ intro_pattern}
+             injection as {+ intro_pattern}
+             einjection @term {? with @bindings_list} as {+ intro_pattern}
+             einjection @num as {+ intro_pattern}
+             einjection as {+ intro_pattern}
+
+      These variants apply :n:`intros {+ @intro_pattern}` after the call to
+      :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 a hypothesis.
 
    .. flag:: Structural Injection
 
@@ -2444,8 +2464,10 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    subgoals.
 
    .. exn:: The @term provided does not end with an equation.
+      :undocumented:
 
    .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal.
+      :undocumented:
 
    .. tacv:: rewrite -> @term
 
@@ -2522,6 +2544,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    :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.
+      :undocumented:
 
    .. tacv:: replace @term with @term’ by @tactic
 
@@ -2544,8 +2567,8 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       the form :n:`@term’ = @term`
 
    .. tacv:: replace @term {? with @term} in clause {? by @tactic}
-   .. tacv:: replace -> @term in clause
-   .. tacv:: replace <- @term in clause
+             replace -> @term in clause
+             replace <- @term in clause
 
       Acts as before but the replacements take place in the specified clause (see
       :ref:`performingcomputations`) and not only in the conclusion of the goal. The
@@ -2658,6 +2681,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    convertible.
 
    .. exn:: Not convertible.
+      :undocumented:
 
    .. tacv:: change @term with @term’
 
@@ -2670,6 +2694,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible.
 
       .. exn:: Too few occurrences.
+         :undocumented:
 
    .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident
 
@@ -2712,12 +2737,9 @@ following:
 For backward compatibility, the notation :n:`in {+ @ident}` performs
 the conversion in hypotheses :n:`{+ @ident}`.
 
-.. tacn:: cbv {* flag}
-   :name: cbv
-.. tacn:: lazy {* flag}
-   :name: lazy
-.. tacn:: compute
-   :name: compute
+.. tacn:: cbv {* @flag}
+          lazy {* @flag}
+   :name: cbv; lazy
 
    These parameterized reduction tactics apply to any goal and perform
    the normalization of the goal according to the specified flags. In
@@ -2765,7 +2787,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
    evaluating purely computational expressions (i.e. with little dead code).
 
 .. tacv:: compute
-.. tacv:: cbv
+          cbv
+   :name: compute; _
 
    These are synonyms for ``cbv beta delta iota zeta``.
 
@@ -2774,17 +2797,17 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This is a synonym for ``lazy beta delta iota zeta``.
 
 .. tacv:: compute {+ @qualid}
-.. tacv:: cbv {+ @qualid}
+          cbv {+ @qualid}
 
    These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`.
 
 .. tacv:: compute -{+ @qualid}
-.. tacv:: cbv -{+ @qualid}
+          cbv -{+ @qualid}
 
    These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`.
 
 .. tacv:: lazy {+ @qualid}
-.. tacv:: lazy -{+ @qualid}
+          lazy -{+ @qualid}
 
    These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta`
    and :n:`lazy beta delta -{+ @qualid} iota zeta`.
@@ -2864,9 +2887,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
  on transparency and opacity).
 
 .. tacn:: cbn
-   :name: cbn
-.. tacn:: simpl
-   :name: simpl
+          simpl
+   :name: cbn; simpl
 
    These tactics apply to any goal. They try to reduce a term to
    something still readable instead of fully normalizing it. They perform
@@ -2962,7 +2984,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :g:`succ t` is reduced to :g:`S t`.
 
 .. tacv:: cbn {+ @qualid}
-.. tacv:: cbn -{+ @qualid}
+          cbn -{+ @qualid}
 
    These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta`
    and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`).
@@ -2978,16 +3000,17 @@ the conversion in hypotheses :n:`{+ @ident}`.
    matching :n:`@pattern` in the current goal.
 
    .. exn:: Too few occurrences.
+      :undocumented:
 
 .. tacv:: simpl @qualid
-.. tacv:: simpl @string
+          simpl @string
 
-   This applies ``simpl`` only to the applicative subterms whose head occurrence
+   This applies :tacn:`simpl` only to the applicative subterms whose head occurrence
    is the unfoldable constant :n:`@qualid` (the constant can be referred to by
    its notation using :n:`@string` if such a notation exists).
 
 .. tacv:: simpl @qualid at {+ @num}
-.. tacv:: simpl @string at {+ @num}
+          simpl @string at {+ @num}
 
    This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose
    head occurrence is :n:`@qualid` (or :n:`@string`).
@@ -3008,6 +3031,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :math:`\beta`:math:`\iota`-normal form.
 
 .. exn:: @qualid does not denote an evaluable constant.
+   :undocumented:
 
 .. tacv:: unfold @qualid in @ident
 
@@ -3025,8 +3049,10 @@ the conversion in hypotheses :n:`{+ @ident}`.
    unfolded. Occurrences are located from left to right.
 
    .. exn:: Bad occurrence number of @qualid.
+      :undocumented:
 
    .. exn:: @qualid does not occur.
+      :undocumented:
 
 .. tacv:: unfold @string
 
@@ -3117,6 +3143,7 @@ Conversion tactics applied to hypotheses
    Example: :n:`unfold not in (type of H1) (type of H3)`.
 
 .. exn:: No such hypothesis: @ident.
+   :undocumented:
 
 
 .. _automation:
@@ -3127,38 +3154,41 @@ Automation
 .. tacn:: auto
    :name: auto
 
-This tactic implements a Prolog-like resolution procedure to solve the
-current goal. It first tries to solve the goal using the assumption
-tactic, then it reduces the goal to an atomic one using intros and
-introduces the newly generated hypotheses as hints. Then it looks at
-the list of tactics associated to the head symbol of the goal and
-tries to apply one of them (starting from the tactics with lower
-cost). This process is recursively applied to the generated subgoals.
+   This tactic implements a Prolog-like resolution procedure to solve the
+   current goal. It first tries to solve the goal using the assumption
+   tactic, then it reduces the goal to an atomic one using intros and
+   introduces the newly generated hypotheses as hints. Then it looks at
+   the list of tactics associated to the head symbol of the goal and
+   tries to apply one of them (starting from the tactics with lower
+   cost). This process is recursively applied to the generated subgoals.
 
-By default, auto only uses the hypotheses of the current goal and the
-hints of the database named core.
+   By default, auto only uses the hypotheses of the current goal and the
+   hints of the database named core.
 
 .. tacv:: auto @num
 
-  Forces the search depth to be :n:`@num`. The maximal search depth
-  is `5` by default.
+   Forces the search depth to be :token:`num`. The maximal search depth
+   is 5 by default.
 
 .. tacv:: auto with {+ @ident}
 
-  Uses the hint databases :n:`{+ @ident}` in addition to the database core. See
-  :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of
-  pre-defined databases and the way to create or extend a database.
+   Uses the hint databases :n:`{+ @ident}` in addition to the database core.
+
+   .. seealso::
+      :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of
+      pre-defined databases and the way to create or extend a database.
 
 .. tacv:: auto with *
 
-  Uses all existing hint databases. See
-  :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
+   Uses all existing hint databases.
+
+   .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
-.. tacv:: auto using {+ @lemma}
+.. tacv:: auto using {+ @ident__i} {? with {+ @ident } }
 
-  Uses :n:`{+ @lemma}` in addition to hints (can be combined with the with
-  :n:`@ident` option).  If :n:`@lemma` is an inductive type, it is the
-  collection of its constructors which is added as hints.
+   Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an
+   inductive type, it is the collection of its constructors which are added
+   as hints.
 
 .. tacv:: info_auto
 
@@ -3184,13 +3214,24 @@ hints of the database named core.
    equalities like :g:`X=X`.
 
 .. tacv:: trivial with {+ @ident}
+   :undocumented:
+
 .. tacv:: trivial with *
+   :undocumented:
+
 .. tacv:: trivial using {+ @lemma}
+   :undocumented:
+
 .. tacv:: debug trivial
    :name: debug trivial
+   :undocumented:
+
 .. tacv:: info_trivial
    :name: info_trivial
+   :undocumented:
+
 .. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}}
+   :undocumented:
 
 .. note::
   :tacn:`auto` either solves completely the goal or else leaves it
@@ -3210,26 +3251,26 @@ the :tacn:`auto` and :tacn:`trivial` tactics:
 .. tacn:: eauto
    :name: eauto
 
-This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try
-resolution hints which would leave existential variables in the goal,
-:tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply`
-where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto`
-can solve such a goal:
+   This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try
+   resolution hints which would leave existential variables in the goal,
+   :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply`
+   where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto`
+   can solve such a goal:
 
-.. example::
+   .. example::
 
-   .. coqtop:: all
+      .. coqtop:: all
 
-      Hint Resolve ex_intro.
-      Goal forall P:nat -> Prop, P 0 -> exists n, P n.
-      eauto.
+         Hint Resolve ex_intro.
+         Goal forall P:nat -> Prop, P 0 -> exists n, P n.
+         eauto.
 
-Note that ``ex_intro`` should be declared as a hint.
+      Note that ``ex_intro`` should be declared as a hint.
 
 
 .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}}
 
-  The various options for eauto are the same as for auto.
+   The various options for :tacn:`eauto` are the same as for :tacn:`auto`.
 
 :tacn:`eauto` also obeys the following options:
 
@@ -3243,13 +3284,12 @@ Note that ``ex_intro`` should be declared as a hint.
 .. tacn:: autounfold with {+ @ident}
    :name: autounfold
 
-
-This tactic unfolds constants that were declared through a ``Hint Unfold``
-in the given databases.
+   This tactic unfolds constants that were declared through a :cmd:`Hint Unfold`
+   in the given databases.
 
 .. tacv:: autounfold with {+ @ident} in clause
 
-  Performs the unfolding in the given clause.
+   Performs the unfolding in the given clause.
 
 .. tacv:: autounfold with *
 
@@ -3258,18 +3298,18 @@ in the given databases.
 .. tacn:: autorewrite with {+ @ident}
    :name: autorewrite
 
-This tactic [4]_ carries out rewritings according to the rewriting rule
-bases :n:`{+ @ident}`.
+   This tactic [4]_ carries out rewritings according to the rewriting rule
+   bases :n:`{+ @ident}`.
 
-Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until
-it fails. Once all the rules have been processed, if the main subgoal has
-progressed (e.g., if it is distinct from the initial main goal) then the rules
-of this base are processed again. If the main subgoal has not progressed then
-the next base is processed. For the bases, the behavior is exactly similar to
-the processing of the rewriting rules.
+   Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until
+   it fails. Once all the rules have been processed, if the main subgoal has
+   progressed (e.g., if it is distinct from the initial main goal) then the rules
+   of this base are processed again. If the main subgoal has not progressed then
+   the next base is processed. For the bases, the behavior is exactly similar to
+   the processing of the rewriting rules.
 
-The rewriting rule bases are built with the ``Hint Rewrite vernacular``
-command.
+   The rewriting rule bases are built with the :cmd:`Hint Rewrite`
+   command.
 
 .. warning::
 
@@ -3435,6 +3475,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       itself.
 
    .. exn:: @term cannot be used as a hint
+      :undocumented:
 
    .. cmdv:: Immediate {+ @term}
 
@@ -3448,6 +3489,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor.
 
    .. exn:: @ident is not an inductive type
+      :undocumented:
 
    .. cmdv:: Hint Constructors {+ @ident}
 
@@ -3616,16 +3658,16 @@ use one or several databases specific to your development.
 
 .. cmd:: Remove Hints {+ @term} : {+ @ident}
 
-This command removes the hints associated to terms :n:`{+ @term}` in databases
-:n:`{+ @ident}`.
+   This command removes the hints associated to terms :n:`{+ @term}` in databases
+   :n:`{+ @ident}`.
 
 .. _printhint:
 
 .. cmd:: Print Hint
 
-This command displays all hints that apply to the current goal. It
-fails if no proof is being edited, while the two variants can be used
-at every moment.
+   This command displays all hints that apply to the current goal. It
+   fails if no proof is being edited, while the two variants can be used
+   at every moment.
 
 **Variants:**
 
@@ -3753,17 +3795,17 @@ Decision procedures
 .. tacn:: tauto
    :name: tauto
 
-This tactic implements a decision procedure for intuitionistic propositional
-calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
-:cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an
-intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and
-logical equivalence but does not unfold any other definition.
-
-The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
-fail:
+   This tactic implements a decision procedure for intuitionistic propositional
+   calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
+   :cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an
+   intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and
+   logical equivalence but does not unfold any other definition.
 
 .. example::
 
+   The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
+   fail:
+
    .. coqtop:: reset all
 
       Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
@@ -3799,27 +3841,24 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
 .. tacn:: intuition @tactic
    :name: intuition
 
-The tactic :tacn:`intuition` takes advantage of the search-tree built by the
-decision procedure involved in the tactic :tacn:`tauto`. It uses this
-information to generate a set of subgoals equivalent to the original one (but
-simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If
-this tactic fails on some goals then :tacn:`intuition` fails. In fact,
-:tacn:`tauto` is simply :g:`intuition fail`.
+   The tactic :tacn:`intuition` takes advantage of the search-tree built by the
+   decision procedure involved in the tactic :tacn:`tauto`. It uses this
+   information to generate a set of subgoals equivalent to the original one (but
+   simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If
+   this tactic fails on some goals then :tacn:`intuition` fails. In fact,
+   :tacn:`tauto` is simply :g:`intuition fail`.
 
-For instance, the tactic :g:`intuition auto` applied to the goal
-
-::
-
-    (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O
+   .. example::
 
+      For instance, the tactic :g:`intuition auto` applied to the goal::
 
-internally replaces it by the equivalent one:
-::
+         (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O
 
-    (forall (x:nat), P x), B |- P O
+      internally replaces it by the equivalent one::
 
+        (forall (x:nat), P x), B |- P O
 
-and then uses :tacn:`auto` which completes the proof.
+      and then uses :tacn:`auto` which completes the proof.
 
 Originally due to César Muñoz, these tactics (:tacn:`tauto` and
 :tacn:`intuition`) have been completely re-engineered by David Delahaye using
@@ -3849,25 +3888,25 @@ some incompatibilities.
 .. tacn:: rtauto
    :name: rtauto
 
-The :tacn:`rtauto` tactic solves propositional tautologies similarly to what
-:tacn:`tauto` does. The main difference is that the proof term is built using a
-reflection scheme applied to a sequent calculus proof of the goal.  The search
-procedure is also implemented using a different technique.
+   The :tacn:`rtauto` tactic solves propositional tautologies similarly to what
+   :tacn:`tauto` does. The main difference is that the proof term is built using a
+   reflection scheme applied to a sequent calculus proof of the goal.  The search
+   procedure is also implemented using a different technique.
 
-Users should be aware that this difference may result in faster proof-search
-but slower proof-checking, and :tacn:`rtauto` might not solve goals that
-:tacn:`tauto` would be able to solve (e.g. goals involving universal
-quantifiers).
+   Users should be aware that this difference may result in faster proof-search
+   but slower proof-checking, and :tacn:`rtauto` might not solve goals that
+   :tacn:`tauto` would be able to solve (e.g. goals involving universal
+   quantifiers).
 
-Note that this tactic is only available after a ``Require Import Rtauto``.
+   Note that this tactic is only available after a ``Require Import Rtauto``.
 
 .. tacn:: firstorder
    :name: firstorder
 
-The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to
-first- order reasoning, written by Pierre Corbineau. It is not restricted to
-usual logical connectives but instead may reason about any first-order class
-inductive definition.
+   The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to
+   first- order reasoning, written by Pierre Corbineau. It is not restricted to
+   usual logical connectives but instead may reason about any first-order class
+   inductive definition.
 
 .. opt:: Firstorder Solver @tactic
    :name: Firstorder Solver
@@ -3906,20 +3945,20 @@ inductive definition.
 .. tacn:: congruence
    :name: congruence
 
-The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard
-Nelson and Oppen congruence closure algorithm, which is a decision procedure
-for ground equalities with uninterpreted symbols. It also includes
-constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal
-is a non-quantified equality, congruence tries to prove it with non-quantified
-equalities in the context. Otherwise it tries to infer a discriminable equality
-from those in the context. Alternatively, congruence tries to prove that a
-hypothesis is equal to the goal or to the negation of another hypothesis.
-
-:tacn:`congruence` is also able to take advantage of hypotheses stating
-quantified equalities, but you have to provide a bound for the number of extra
-equalities generated that way. Please note that one of the sides of the
-equality must contain all the quantified variables in order for congruence to
-match against it.
+   The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard
+   Nelson and Oppen congruence closure algorithm, which is a decision procedure
+   for ground equalities with uninterpreted symbols. It also includes
+   constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal
+   is a non-quantified equality, congruence tries to prove it with non-quantified
+   equalities in the context. Otherwise it tries to infer a discriminable equality
+   from those in the context. Alternatively, congruence tries to prove that a
+   hypothesis is equal to the goal or to the negation of another hypothesis.
+
+   :tacn:`congruence` is also able to take advantage of hypotheses stating
+   quantified equalities, but you have to provide a bound for the number of extra
+   equalities generated that way. Please note that one of the sides of the
+   equality must contain all the quantified variables in order for congruence to
+   match against it.
 
 .. example::
 
@@ -3980,7 +4019,10 @@ succeeds, and results in an error otherwise.
    conversion, casts and universe constraints. It may unify universes.
 
 .. exn:: Not equal.
+   :undocumented:
+
 .. exn:: Not equal (due to universes).
+   :undocumented:
 
 .. tacn:: constr_eq_strict @term @term
    :name: constr_eq_strict
@@ -3990,7 +4032,10 @@ succeeds, and results in an error otherwise.
    constraints.
 
 .. exn:: Not equal.
+   :undocumented:
+
 .. exn:: Not equal (due to universes).
+   :undocumented:
 
 .. tacn:: unify @term @term
    :name: unify
@@ -3999,6 +4044,7 @@ succeeds, and results in an error otherwise.
    instantiating existential variables.
 
 .. exn:: Unable to unify @term with @term.
+   :undocumented:
 
 .. tacv:: unify @term @term with @ident
 
@@ -4013,6 +4059,7 @@ succeeds, and results in an error otherwise.
    by :tacn:`eapply` and some other tactics.
 
 .. exn:: Not an evar.
+   :undocumented:
 
 .. tacn:: has_evar @term
    :name: has_evar
@@ -4022,6 +4069,7 @@ succeeds, and results in an error otherwise.
    scans all subterms, including those under binders.
 
 .. exn:: No evars.
+   :undocumented:
 
 .. tacn:: is_var @term
    :name: is_var
@@ -4030,6 +4078,7 @@ succeeds, and results in an error otherwise.
    the current goal context or in the opened sections.
 
 .. exn:: Not a variable or hypothesis.
+   :undocumented:
 
 
 .. _equality:
@@ -4041,45 +4090,46 @@ Equality
 .. tacn:: f_equal
    :name: f_equal
 
-This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n`
-:g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`.  Using :tacn:`f_equal` on such a goal
-leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up
-to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones
-(e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically
-solved by :tacn:`f_equal`.
+   This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n`
+   :g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`.  Using :tacn:`f_equal` on such a goal
+   leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up
+   to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones
+   (e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically
+   solved by :tacn:`f_equal`.
 
 
 .. tacn:: reflexivity
    :name: reflexivity
 
-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 refl_equal``.
+   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 refl_equal``.
 
-.. exn:: The conclusion is not a substitutive equation.
+   .. exn:: The conclusion is not a substitutive equation.
+      :undocumented:
 
-.. exn:: Unable to unify ... with ...
+   .. exn:: Unable to unify ... with ...
+      :undocumented:
 
 
 .. tacn:: symmetry
    :name: symmetry
 
-This tactic applies to a goal that has the form :g:`t=u` and changes it into
-:g:`u=t`.
+   This tactic applies to a goal that has the form :g:`t=u` and changes it into
+   :g:`u=t`.
 
 
 .. tacv:: symmetry in @ident
 
-  If the statement of the hypothesis ident has the form :g:`t=u`, the tactic
-  changes it to :g:`u=t`.
-
+   If the statement of the hypothesis ident has the form :g:`t=u`, the tactic
+   changes it to :g:`u=t`.
 
 
 .. tacn:: transitivity @term
    :name: transitivity
 
-This tactic applies to a goal that has the form :g:`t=u` and transforms it
-into the two subgoals :n:`t=@term` and :n:`@term=u`.
+   This tactic applies to a goal that has the form :g:`t=u` and transforms it
+   into the two subgoals :n:`t=@term` and :n:`@term=u`.
 
 
 Equality and inductive sets
@@ -4133,10 +4183,10 @@ symbol :g:`=`.
    instantiate parameters or hypotheses of :n:`@term`.
 
 .. tacv:: esimplify_eq @num
-.. tacv:: esimplify_eq @term {? with @bindings_list}
-   :name: esimplify_eq
+          esimplify_eq @term {? with @bindings_list}
+   :name: esimplify_eq; _
 
-   This works the same as ``simplify_eq`` but if the type of :n:`@term`, or the
+   This works the same as :tacn:`simplify_eq` 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.
 
@@ -4168,35 +4218,35 @@ Inversion
 .. tacn:: functional inversion @ident
    :name: functional inversion
 
-:tacn:`functional inversion` is a tactic that performs inversion on hypothesis
-:n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid
-{+ @term}` where :n:`@qualid` must have been defined using Function (see
-:ref:`advanced-recursive-functions`). Note that this tactic is only
-available after a ``Require Import FunInd``.
+   :tacn:`functional inversion` is a tactic that performs inversion on hypothesis
+   :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid
+   {+ @term}` where :n:`@qualid` must have been defined using Function (see
+   :ref:`advanced-recursive-functions`). Note that this tactic is only
+   available after a ``Require Import FunInd``.
 
+   .. exn:: Hypothesis @ident must contain at least one Function.
+      :undocumented:
 
-.. exn:: Hypothesis @ident must contain at least one Function.
-.. exn:: Cannot find inversion information for hypothesis @ident.
+   .. exn:: Cannot find inversion information for hypothesis @ident.
 
-  This error may be raised when some inversion lemma failed to be generated by
-  Function.
+      This error may be raised when some inversion lemma failed to be generated by
+      Function.
 
 
-.. tacv:: functional inversion @num
+   .. tacv:: functional inversion @num
 
-  This does the same thing as :n:`intros until @num` folowed by
-  :n:`functional inversion @ident` where :token:`ident` is the
-  identifier for the last introduced hypothesis.
+      This does the same thing as :n:`intros until @num` folowed by
+      :n:`functional inversion @ident` where :token:`ident` is the
+      identifier for the last introduced hypothesis.
 
-.. tacv:: functional inversion ident qualid
-.. tacv:: functional inversion num qualid
+   .. tacv:: functional inversion @ident @qualid
+             functional inversion @num @qualid
 
-  If the hypothesis :n:`@ident` (or :n:`@num`) has a type of the form
-  :n:`@qualid`:sub:`1` :n:`@term`:sub:`1` ... :n:`@term`:sub:`n` :n:`=
-  @qualid`:sub:`2` :n:`@term`:sub:`n+1` ... :n:`@term`:sub:`n+m` where
-  :n:`@qualid`:sub:`1` and :n:`@qualid`:sub:`2` are valid candidates to
-  functional inversion, this variant allows choosing which :n:`@qualid` is
-  inverted.
+      If the hypothesis :token:`ident` (or :token:`num`) has a type of the form
+      :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
+      :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
+      functional inversion, this variant allows choosing which :token:`qualid`
+      is inverted.
 
 Classical tactics
 -----------------
@@ -4206,15 +4256,14 @@ loaded. A few more tactics are available. Make sure to load the module
 using the ``Require Import`` command.
 
 .. tacn:: classical_left
-   :name: classical_left
-.. tacv:: classical_right
-   :name: classical_right
+          classical_right
+   :name: classical_left; classical_right
 
-   The tactics ``classical_left`` and ``classical_right`` are the analog of the
-   left and right but using classical logic. They can only be used for
-   disjunctions. Use ``classical_left`` to prove the left part of the
+   These tactics are the analog of :tacn:`left` and :tacn:`right`
+   but using classical logic. They can only be used for
+   disjunctions. Use :tacn:`classical_left` to prove the left part of the
    disjunction with the assumption that the negation of right part holds.
-   Use ``classical_right`` to prove the right part of the disjunction with
+   Use :tacn:`classical_right` to prove the right part of the disjunction with
    the assumption that the negation of left part holds.
 
 .. _tactics-automating:
@@ -4226,93 +4275,92 @@ Automating
 .. tacn:: btauto
    :name: btauto
 
-The tactic :tacn:`btauto` implements a reflexive solver for boolean
-tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are
-constructed over the following grammar:
+   The tactic :tacn:`btauto` implements a reflexive solver for boolean
+   tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are
+   constructed over the following grammar:
 
-.. _btauto_grammar:
+   .. _btauto_grammar:
 
-  .. productionlist:: `sentence`
-     t : x
-       :∣ true
-       :∣ false
-       :∣ orb t1 t2
-       :∣ andb t1 t2
-       :∣ xorb t1 t2
-       :∣ negb t
-       :∣ if t1 then t2 else t3
+   .. productionlist:: `sentence`
+      t : x
+        :∣ true
+        :∣ false
+        :∣ orb t1 t2
+        :∣ andb t1 t2
+        :∣ xorb t1 t2
+        :∣ negb t
+        :∣ if t1 then t2 else t3
 
-  Whenever the formula supplied is not a tautology, it also provides a
-  counter-example.
+   Whenever the formula supplied is not a tautology, it also provides a
+   counter-example.
 
-  Internally, it uses a system very similar to the one of the ring
-  tactic.
+   Internally, it uses a system very similar to the one of the ring
+   tactic.
 
-  Note that this tactic is only available after a ``Require Import Btauto``.
+   Note that this tactic is only available after a ``Require Import Btauto``.
 
-.. exn:: Cannot recognize a boolean equality.
+   .. exn:: Cannot recognize a boolean equality.
 
-   The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
-   doesn't introduce variables into the context on its own.
+      The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
+      doesn't introduce variables into the context on its own.
 
 .. tacn:: omega
    :name: omega
 
-The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision
-procedure for Presburger arithmetic. It solves quantifier-free
-formulas built with `~`, `\/`, `/\`, `->` on top of equalities,
-inequalities and disequalities on both the type :g:`nat` of natural numbers
-and :g:`Z` of binary integers. This tactic must be loaded by the command
-``Require Import Omega``. See the additional documentation about omega
-(see Chapter :ref:`omega`).
+   The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision
+   procedure for Presburger arithmetic. It solves quantifier-free
+   formulas built with `~`, `\/`, `/\`, `->` on top of equalities,
+   inequalities and disequalities on both the type :g:`nat` of natural numbers
+   and :g:`Z` of binary integers. This tactic must be loaded by the command
+   ``Require Import Omega``. See the additional documentation about omega
+   (see Chapter :ref:`omega`).
 
 
 .. tacn:: ring
    :name: ring
+
+   This tactic solves equations upon polynomial expressions of a ring
+   (or semiring) structure. It proceeds by normalizing both hand sides
+   of the equation (w.r.t. associativity, commutativity and
+   distributivity, constant propagation) and comparing syntactically the
+   results.
+
 .. tacn:: ring_simplify {+ @term}
    :name: ring_simplify
 
-The :n:`ring` tactic solves equations upon polynomial expressions of a ring
-(or semiring) structure. It proceeds by normalizing both hand sides
-of the equation (w.r.t. associativity, commutativity and
-distributivity, constant propagation) and comparing syntactically the
-results.
-
-:n:`ring_simplify` applies the normalization procedure described above to
-the given terms. The tactic then replaces all occurrences of the terms
-given in the conclusion of the goal by their normal forms. If no term
-is given, then the conclusion should be an equation and both hand
-sides are normalized.
+   This tactic applies the normalization procedure described above to
+   the given terms. The tactic then replaces all occurrences of the terms
+   given in the conclusion of the goal by their normal forms. If no term
+   is given, then the conclusion should be an equation and both hand
+   sides are normalized.
 
 See :ref:`Theringandfieldtacticfamilies` for more information on
 the tactic and how to declare new ring structures. All declared field structures
 can be printed with the ``Print Rings`` command.
 
 .. tacn:: field
-   :name: field
-.. tacn:: field_simplify {+ @term}
-   :name: field_simplify
-.. tacn:: field_simplify_eq
-   :name: field_simplify_eq
-
-The field tactic is built on the same ideas as ring: this is a
-reflexive tactic that solves or simplifies equations in a field
-structure. The main idea is to reduce a field expression (which is an
-extension of ring expressions with the inverse and division
-operations) to a fraction made of two polynomial expressions.
-
-Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}`
-replaces the provided terms by their reduced fraction.
-:n:`field_simplify_eq` applies when the conclusion is an equation: it
-simplifies both hand sides and multiplies so as to cancel
-denominators. So it produces an equation without division nor inverse.
-
-All of these 3 tactics may generate a subgoal in order to prove that
-denominators are different from zero.
-
-See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to
-declare new field structures. All declared field structures can be
-printed with the Print Fields command.
+          field_simplify {+ @term}
+          field_simplify_eq
+   :name: field; field_simplify; field_simplify_eq
+
+   The field tactic is built on the same ideas as ring: this is a
+   reflexive tactic that solves or simplifies equations in a field
+   structure. The main idea is to reduce a field expression (which is an
+   extension of ring expressions with the inverse and division
+   operations) to a fraction made of two polynomial expressions.
+
+   Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}`
+   replaces the provided terms by their reduced fraction.
+   :n:`field_simplify_eq` applies when the conclusion is an equation: it
+   simplifies both hand sides and multiplies so as to cancel
+   denominators. So it produces an equation without division nor inverse.
+
+   All of these 3 tactics may generate a subgoal in order to prove that
+   denominators are different from zero.
+
+   See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to
+   declare new field structures. All declared field structures can be
+   printed with the Print Fields command.
 
 .. example::
 
@@ -4373,16 +4421,16 @@ Non-logical tactics
 .. tacn:: revgoals
    :name: revgoals
 
-This tactics reverses the list of the focused goals.
+   This tactics reverses the list of the focused goals.
 
-.. example::
+   .. example::
 
-   .. coqtop:: all reset
+      .. coqtop:: all reset
 
-      Parameter P : nat -> Prop.
-      Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
-      repeat split.
-      all: revgoals.
+         Parameter P : nat -> Prop.
+         Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5.
+         repeat split.
+         all: revgoals.
 
 .. tacn:: shelve
    :name: shelve
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a69cf209c7..4bc85f386d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -20,10 +20,13 @@ Displaying
    Error messages:
 
    .. exn:: @qualid not a defined object.
+      :undocumented:
 
    .. exn:: Universe instance should have length @num.
+      :undocumented:
 
    .. exn:: This object does not support universe names.
+      :undocumented:
 
 
    .. cmdv:: Print Term @qualid
@@ -81,9 +84,9 @@ and tables:
 * A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`.
 * An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`.
 * A :production:`table` contains a set of strings or qualids.
-* In addition, some commands provide settings, such as :cmd:`Extraction Language OCaml`.
+* In addition, some commands provide settings, such as :cmd:`Extraction Language`.
 
-.. FIXME Convert `Extraction Language OCaml` to an option.
+.. FIXME Convert "Extraction Language" to an option.
 
 Flags, options and tables are identified by a series of identifiers, each with an initial
 capital letter.
@@ -538,8 +541,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
       will use the default extension ``.v``.
 
    .. cmdv:: Load Verbose @ident
-
-   .. cmdv:: Load Verbose @string
+             Load Verbose @string
 
       Display, while loading,
       the answers of |Coq| to each command (including tactics) contained in
@@ -548,10 +550,13 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
       .. seealso:: Section :ref:`controlling-display`.
 
    .. exn:: Can’t find file @ident on loadpath.
+      :undocumented:
 
    .. exn:: Load is not supported inside proofs.
+      :undocumented:
 
    .. exn:: Files processed by Load cannot leave open proofs.
+      :undocumented:
 
 .. _compiled-files:
 
@@ -620,6 +625,7 @@ file is a particular case of module called *library file*.
       comes from a given package by making explicit its absolute root.
 
    .. exn:: Cannot load qualid: no physical path bound to dirpath.
+      :undocumented:
 
    .. exn:: Cannot find library foo in loadpath.
 
@@ -684,8 +690,10 @@ file is a particular case of module called *library file*.
       where they occur, even if outside a section.
 
    .. exn:: File not found on loadpath: @string.
+      :undocumented:
 
    .. exn:: Loading of ML object file forbidden in a native Coq.
+      :undocumented:
 
 
 .. cmd:: Print ML Modules
@@ -812,6 +820,7 @@ interactively, they cannot be part of a vernacular file loaded via
    over the name of a module or of an object inside a module.
 
    .. exn:: @ident: no such entry.
+      :undocumented:
 
    .. cmdv:: Reset Initial
 
@@ -953,6 +962,7 @@ Quitting and debugging
    it prints a message indicating that the failure did not occur.
 
    .. exn:: The command has not failed!
+      :undocumented:
 
 
 .. _controlling-display:
@@ -1136,6 +1146,7 @@ described first.
    variable nor a constant.
 
    .. exn:: The reference is not unfoldable.
+      :undocumented:
 
    .. cmdv:: Print Strategies
 
@@ -1166,41 +1177,41 @@ Controlling the locality of commands
 
 
 .. 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:
-
-
-+ Commands whose default is to extend their effect both outside the
-  section and the module or library file they occur in.  For these
-  commands, the Local modifier limits the effect of the command to the
-  current section or module it occurs in.  As an example, the :cmd:`Coercion`
-  and :cmd:`Strategy` commands belong to this category.
-+ Commands whose default behavior is to stop their effect at the end
-  of the section they occur in but to extend their effect outside the module or
-  library file they occur in. For these commands, the Local modifier limits the
-  effect of the command to the current module if the command does not occur in a
-  section and the Global modifier extends the effect outside the current
-  sections and current module if the command occurs in a section. As an example,
-  the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
-  to this category. Notice that a subclass of these commands do not support
-  extension of their scope outside sections at all and the Global modifier is not
-  applicable to them.
-+ Commands whose default behavior is to stop their effect at the end
-  of the section or module they occur in.  For these commands, the ``Global``
-  modifier extends their effect outside the sections and modules they
-  occur in.  The :cmd:`Transparent` and :cmd:`Opaque`
-  (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands
-  belong to this category.
-+ Commands whose default behavior is to extend their effect outside
-  sections but not outside modules when they occur in a section and to
-  extend their effect outside the module or library file they occur in
-  when no section contains them.For these commands, the Local modifier
-  limits the effect to the current section or module while the Global
-  modifier extends the effect outside the module even when the command
-  occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
-  category.
+         Global @command
+
+   Some commands support a Local or Global prefix modifier to control the
+   scope of their effect. There are four kinds of commands:
+
+
+   + Commands whose default is to extend their effect both outside the
+     section and the module or library file they occur in.  For these
+     commands, the Local modifier limits the effect of the command to the
+     current section or module it occurs in.  As an example, the :cmd:`Coercion`
+     and :cmd:`Strategy` commands belong to this category.
+   + Commands whose default behavior is to stop their effect at the end
+     of the section they occur in but to extend their effect outside the module or
+     library file they occur in. For these commands, the Local modifier limits the
+     effect of the command to the current module if the command does not occur in a
+     section and the Global modifier extends the effect outside the current
+     sections and current module if the command occurs in a section. As an example,
+     the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
+     to this category. Notice that a subclass of these commands do not support
+     extension of their scope outside sections at all and the Global modifier is not
+     applicable to them.
+   + Commands whose default behavior is to stop their effect at the end
+     of the section or module they occur in.  For these commands, the ``Global``
+     modifier extends their effect outside the sections and modules they
+     occur in.  The :cmd:`Transparent` and :cmd:`Opaque`
+     (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands
+     belong to this category.
+   + Commands whose default behavior is to extend their effect outside
+     sections but not outside modules when they occur in a section and to
+     extend their effect outside the module or library file they occur in
+     when no section contains them.For these commands, the Local modifier
+     limits the effect to the current section or module while the Global
+     modifier extends the effect outside the module even when the command
+     occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
+     category.
 
 .. _exposing-constants-to-ocaml-libraries: