[sphinx] Fix many warnings.

Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.

4 files changed, 137 insertions, 117 deletions

diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 932f96788..fda20bff3 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -6,6 +6,8 @@ Detailed examples of tactics
 This chapter presents detailed examples of certain tactics, to
 illustrate their behavior.
 
+.. _dependent-induction:
+
 dependent induction
 -------------------
 
@@ -316,7 +318,7 @@ explicit proof terms:
 
 This concludes our example.
 
-See also: The ``induction`` :ref:`TODO-9-induction`, ``case`` :ref:`TODO-9-induction` and ``inversion`` :ref:`TODO-8.14-inversion` tactics.
+See also: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics.
 
 
 autorewrite
@@ -403,6 +405,8 @@ Example 2: Mac Carthy function
    autorewrite with base1 using reflexivity || simpl.
 
 
+.. _quote:
+
 quote
 -----
 
@@ -544,8 +548,7 @@ Combining variables and constants
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 One can have both variables and constants in abstracts terms; for
-example, this is the case for the ``ring`` tactic
-:ref:`TODO-25-ringandfieldtacticfamilies`. Then one must provide to
+example, this is the case for the :tacn:`ring` tactic. Then one must provide to
 ``quote`` a list of *constructors of constants*. For example, if the list
 is ``[O S]`` then closed natural numbers will be considered as constants
 and other terms as variables.
@@ -606,7 +609,7 @@ don’t expect miracles from it!
 
 See also: comments of source file ``plugins/quote/quote.ml``
 
-See also: the ``ring`` tactic :ref:`TODO-25-ringandfieldtacticfamilies`
+See also: the :tacn:`ring` tactic.
 
 
 Using the tactical language
@@ -868,7 +871,7 @@ Deciding type isomorphisms
 A more tricky problem is to decide equalities between types and modulo
 isomorphisms. Here, we choose to use the isomorphisms of the simply
 typed λ-calculus with Cartesian product and unit type (see, for
-example, [:ref:`TODO-45`]). The axioms of this λ-calculus are given below.
+example, :cite:`TODO-45`). The axioms of this λ-calculus are given below.
 
 .. coqtop:: in reset
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index adf3da3eb..c28e85171 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -41,6 +41,8 @@ are called *proof terms*.
 Coq raises this error message when one attempts to use a proof editing command
 out of the proof editing mode.
 
+.. _proof-editing-mode:
+
 Switching on/off the proof editing mode
 -------------------------------------------
 
@@ -119,7 +121,7 @@ closing ``Qed``.
 
 
 See also: ``Proof with tactic.`` in Section
-:ref:`setimpautotactics`.
+:ref:`tactics-implicit-automation`.
 
 
 .. cmd:: Proof using @ident1 ... @identn.
@@ -136,7 +138,7 @@ example if ``T`` is variable and a is a variable of type ``T``, the commands
 
 .. cmdv:: Proof using @ident1 ... @identn with @tactic.
 
-in Section :ref:`setimpautotactics`.
+in Section :ref:`tactics-implicit-automation`.
 
 .. cmdv:: Proof using All.
 
@@ -262,11 +264,11 @@ Existentials`` (described in Section :ref:`requestinginformation`).
 This command is intended to be used to instantiate existential
 variables when the proof is completed but some uninstantiated
 existential variables remain. To instantiate existential variables
-during proof edition, you should use the tactic instantiate.
+during proof edition, you should use the tactic :tacn:`instantiate`.
 
 
 See also: ``instantiate (num:= term).`` in Section
-:ref:`TODO-controllingtheproofflow`.
+:ref:`controllingtheproofflow`.
 See also: ``Grab Existential Variables.`` below.
 
 
@@ -327,6 +329,7 @@ last ``Focus`` command.
 Succeeds if the proof is fully unfocused, fails is there are some
 goals out of focus.
 
+.. _curly-braces:
 
 .. cmd:: %{ %| %}
 
@@ -357,6 +360,8 @@ You are trying to use ``}`` but the current subproof has not been fully solved.
 
 See also error messages about bullets below.
 
+.. _bullets:
+
 Bullets
 ```````
 
@@ -434,6 +439,7 @@ This makes bullets inactive.
 This makes bullets active (this is the default behavior).
 
 
+.. _requestinginformation:
 
 Requesting information
 ----------------------
@@ -456,7 +462,7 @@ Displays only the :n:`@num`-th subgoal.
 Displays the named goal :n:`@ident`. This is useful in
 particular to display a shelved goal but only works if the
 corresponding existential variable has been named by the user
-(see :ref:`exvariables`) as in the following example.
+(see :ref:`existential-variables`) as in the following example.
 
 .. example::
 
@@ -536,7 +542,7 @@ debugging universe inconsistencies.
 
 .. cmd:: Guarded.
 
-Some tactics (e.g. refine :ref:`applyingtheorems`) allow to build proofs using
+Some tactics (e.g. :tacn:`refine` :ref:`applyingtheorems`) 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
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2af73c28e..046efa730 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -24,7 +24,7 @@ Each (sub)goal is denoted with a number. The current goal is numbered
 1. By default, a tactic is applied to the current goal, but one can
 address a particular goal in the list by writing n:tactic which means
 “apply tactic tactic to goal number n”. We can show the list of
-subgoals by typing Show (see Section :ref:`TODO-7.3.1-Show`).
+subgoals by typing Show (see Section :ref:`requestinginformation`).
 
 Since not every rule applies to a given statement, every tactic cannot
 be used to reduce any goal. In other words, before applying a tactic
@@ -36,13 +36,14 @@ extends the folklore notion of tactical) to combine those atomic
 tactics. This chapter is devoted to atomic tactics. The tactic
 language will be described in Chapter :ref:`TODO-9-Thetacticlanguage`.
 
+.. _invocation-of-tactics:
+
 Invocation of tactics
 -------------------------
 
 A tactic is applied as an ordinary command. It may be preceded by a
 goal selector (see Section :ref:`TODO-9.2-Semantics`). If no selector is
-specified, the default selector (see Section
-:ref:`TODO-8.1.1-Setdefaultgoalselector`) is used.
+specified, the default selector is used.
 
 .. _tactic_invocation_grammar:
 
@@ -126,9 +127,9 @@ occurrences have to be selected in the hypotheses named :n:`@ident`. If no numbe
 are given for hypothesis :n:`@ident`, then all the occurrences of `term` in the
 hypothesis are selected. If numbers are given, they refer to occurrences of
 `term` when the term is printed using option ``Set Printing All`` (see
-:ref:`TODO-2.9-Printingconstructionsinfull`), counting from left to right. In
+:ref:`printing_constructions_full`), counting from left to right. In
 particular, occurrences of `term` in implicit arguments (see
-:ref:`TODO-2.7-Implicitarguments`) or coercions (see :ref:`TODO-2.8-Coercions`)
+:ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`)
 are counted.
 
 If a minus sign is given between at and the list of occurrences, it
@@ -154,10 +155,11 @@ Here are some tactics that understand occurrences clauses: ``set``, ``remember``
 , ``induction``, ``destruct``.
 
 
-See also: :ref:`TODO-8.3.7-Managingthelocalcontext`,
-:ref:`TODO-8.5.2-Caseanalysisandinduction`,
-:ref:`TODO-2.9-Printingconstructionsinfull`.
+See also: :ref:`Managingthelocalcontext`,
+:ref:`caseanalysisandinduction`,
+:ref:`printing_constructions_full`.
 
+.. _applyingtheorems:
 
 Applying theorems
 ---------------------
@@ -168,7 +170,7 @@ Applying theorems
 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:`TODO-4.3-Conversionrules`).
+:ref:`Conversion-rules`).
 
 .. exn:: Not an exact proof.
 
@@ -314,7 +316,7 @@ generated by ``apply term``:sub:`i` , starting from the application of
 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:`TODO-2.11-ExistentialVariables`). The instantiation is
+instantiate (see :ref:`Existential-Variables`). The instantiation is
 intended to be found later in the proof.
 
 .. tacv:: simple apply @term.
@@ -598,7 +600,7 @@ Managing the local context
 
 This tactic applies to a goal that is either a product or starts with a let
 binder. If the goal is a product, the tactic implements the "Lam" rule given in
-:ref:`TODO-4.2-Typing-rules` [1]_. If the goal starts with a let binder, then the
+:ref:`Typing-rules` [1]_. If the goal starts with a let binder, then the
 tactic implements a mix of the "Let" and "Conv".
 
 If the current goal is a dependent product :math:`\forall` :g:`x:T, U` (resp
@@ -632,14 +634,14 @@ be applied or the goal is not head-reducible.
 
 .. 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
-   (see :ref:`TODO-2.6.2-Qualified-names`).
+   (see :ref:`Qualified-names`).
 .. tacv:: intros {+ @ident}.
 
    This is equivalent to the composed tactic
    :n:`intro @ident; ... ; intro @ident`. More generally, the ``intros`` tactic
    takes a pattern as argument in order to introduce names for components
    of an inductive definition or to clear introduced hypotheses. This is
-   explained in :ref:`TODO-8.3.2`.
+   explained in :ref:`Managingthelocalcontext`.
 
 .. tacv:: intros until @ident
 
@@ -1067,7 +1069,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
 
    This decomposes record types (inductive types with one constructor, like
    "and" and "exists" and those defined with the Record macro, see
-   :ref:`TODO-2.1`).
+   :ref:`record-types`).
 
 .. _controllingtheproofflow:
 
@@ -1177,7 +1179,7 @@ Controlling the proof flow
 .. tacv:: cut form
 
    This tactic applies to any goal. It implements the non-dependent case of
-   the “App” rule given in :ref:`TODO-4.2`. (This is Modus Ponens inference
+   the “App” rule given in :ref:`typing-rules`. (This is Modus Ponens inference
    rule.) :n:`cut U` transforms the current goal :g:`T` into the two following
    subgoals: :g:`U -> T` and :g:`U`. The subgoal :g:`U -> T` comes first in the
    list of remaining subgoal to prove.
@@ -1268,7 +1270,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
    :n:`refine @term` (preferred alternative).
 
    .. note:: To be able to refer to an existential variable by name, the user
-             must have given the name explicitly (see :ref:`TODO-2.11`).
+             must have given the name explicitly (see :ref:`Existential-Variables`).
 
    .. note:: When you are referring to hypotheses which you did not name
              explicitly, be aware that Coq may make a different decision on how to
@@ -1353,11 +1355,13 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`.
    then required to prove that False is indeed provable in the current
    context. This tactic is a macro for :n:`elimtype False`.
 
+.. _CaseAnalysisAndInduction:
+
 Case analysis and induction
 -------------------------------
 
 The tactics presented in this section implement induction or case
-analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`).
+analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`).
 
 .. tacn:: destruct @term
    :name: destruct
@@ -1746,7 +1750,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`).
    results equivalent to ``inversion`` or ``dependent inversion`` if the
    hypothesis is dependent.
 
-See also :ref:`TODO-10.1-dependentinduction` for a larger example of ``dependent induction``
+See also :ref:`dependentinduction` for a larger example of ``dependent induction``
 and an explanation of the underlying technique.
 
 .. tacn:: function induction (@qualid {+ @term})
@@ -1754,8 +1758,8 @@ and an explanation of the underlying technique.
 
    The tactic functional induction performs case analysis and induction
    following the definition of a function. It makes use of a principle
-   generated by ``Function`` (see :ref:`TODO-2.3-Advancedrecursivefunctions`) or
-   ``Functional Scheme`` (see :ref:`TODO-13.2-Generationofinductionschemeswithfunctionalscheme`).
+   generated by ``Function`` (see :ref:`advanced-recursive-functions`) or
+   ``Functional Scheme`` (see :ref:`functional-scheme`).
    Note that this tactic is only available after a
 
 .. example::
@@ -1781,22 +1785,22 @@ and an explanation of the underlying technique.
    :n:`functional induction (f x1 x2 x3)` is actually a wrapper for
    :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning
    phase, where :n:`@qualid` is the induction principle registered for :g:`f`
-   (by the ``Function`` (see :ref:`TODO-2.3-Advancedrecursivefunctions`) or
-   ``Functional Scheme`` (see :ref:`TODO-13.2-Generationofinductionschemeswithfunctionalscheme`)
+   (by the ``Function`` (see :ref:`advanced-recursive-functions`) or
+   ``Functional Scheme`` (see :ref:`functional-scheme`)
    command) corresponding to the sort of the goal. Therefore
    ``functional induction`` may fail if the induction scheme :n:`@qualid` is not
-   defined. See also :ref:`TODO-2.3-Advancedrecursivefunctions` for the function
+   defined. See also :ref:`advanced-recursive-functions` for the function
    terms accepted by ``Function``.
 
 .. note::
    There is a difference between obtaining an induction scheme
-   for a function by using :g:`Function` (see :ref:`TODO-2.3-Advancedrecursivefunctions`)
+   for a function by using :g:`Function` (see :ref:`advanced-recursive-functions`)
    and by using :g:`Functional Scheme` after a normal definition using
-   :g:`Fixpoint` or :g:`Definition`. See :ref:`TODO-2.3-Advancedrecursivefunctions`
+   :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions`
    for details.
 
-See also: :ref:`TODO-2.3-Advancedrecursivefunctions`
-  :ref:`TODO-13.2-Generationofinductionschemeswithfunctionalscheme`
+See also: :ref:`advanced-recursive-functions`
+  :ref:`functional-scheme`
   :tacn:`inversion`
 
 .. exn:: Cannot find induction information on @qualid
@@ -1902,7 +1906,7 @@ 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:`TODO-13.1-GenerationofinductionprincipleswithScheme`),
+equality has been declared using the command ``Scheme Equality`` (see :ref:`proofschemes-induction-principles`),
 the use of a sigma type is avoided.
 
 .. note::
@@ -1984,7 +1988,7 @@ turned off by setting the option ``Set Keep Proof Equalities``.
 .. note::
    As ``inversion`` proofs may be large in size, we recommend the
    user to stock the lemmas whenever the same instance needs to be
-   inverted several times. See :ref:`TODO-13.3-Generationofinversionprincipleswithderiveinversion`.
+   inverted several times. See :ref:`derive-inversion`.
 
 .. note::
    Part of the behavior of the ``inversion`` tactic is to generate
@@ -2300,7 +2304,7 @@ turned off by setting the option ``Set Keep Proof Equalities``.
    arguments are correct is done only at the time of registering the
    lemma in the environment. To know if the use of induction hypotheses
    is correct at some time of the interactive development of a proof, use
-   the command ``Guarded`` (see :ref:`TODO-7.3.2-Guarded`).
+   the command ``Guarded`` (see Section :ref:`requestinginformation`).
 
 .. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)}
 
@@ -2321,7 +2325,7 @@ turned off by setting the option ``Set Keep Proof Equalities``.
    done only at the time of registering the lemma in the environment. To
    know if the use of coinduction hypotheses is correct at some time of
    the interactive development of a proof, use the command ``Guarded``
-   (see :ref:`TODO-7.3.2-Guarded`).
+   (see Section :ref:`requestinginformation`).
 
 .. tacv:: cofix @ident with {+ (@ident {+ @binder} : @type)}
 
@@ -2335,7 +2339,7 @@ Rewriting expressions
 ---------------------
 
 These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in
-file ``Logic.v`` (see :ref:`TODO-3.1.2-Logic`). The notation for :g:`eq T t u` is
+file ``Logic.v`` (see :ref:`coq-library-logic`). The notation for :g:`eq T t u` is
 simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
 .. tacn:: rewrite @term
@@ -2546,7 +2550,7 @@ then replaces the goal by :n:`R @term @term` and adds a new goal stating
 Lemmas are added to the database using the command ``Declare Left Step @term.``
 The tactic is especially useful for parametric setoids which are not accepted
 as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
-:ref:`TODO-27-Generalizedrewriting`).
+:ref:`Generalizedrewriting`).
 
 .. tacv:: stepl @term by tactic
 
@@ -2564,7 +2568,7 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
    :name: change
 
   This tactic applies to any goal. It implements the rule ``Conv`` given in
-  :ref:`TODO-4.4-Subtypingrules`. :g:`change U` replaces the current goal `T`
+  :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T`
   with `U` providing that `U` is well-formed and that `T` and `U` are
   convertible.
 
@@ -2637,7 +2641,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    the normalization of the goal according to the specified flags. In
    correspondence with the kinds of reduction considered in Coq namely
    :math:`\beta` (reduction of functional application), :math:`\delta`
-   (unfolding of transparent constants, see :ref:`TODO-6.10.2-Transparent`),
+   (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`),
    :math:`\iota` (reduction of
    pattern-matching over a constructed term, and unfolding of :g:`fix` and
    :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the
@@ -2649,7 +2653,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    second case the constant to unfold to all but the ones explicitly mentioned.
    Notice that the ``delta`` flag does not apply to variables bound by a let-in
    construction inside the :n:`@term` itself (use here the ``zeta`` flag). In
-   any cases, opaque constants are not unfolded (see :ref:`TODO-6.10.1-Opaque`).
+   any cases, opaque constants are not unfolded (see :ref:`vernac-controlling-the-reduction-strategies`).
 
    Normalization according to the flags is done by first evaluating the
    head of the expression into a *weak-head* normal form, i.e. until the
@@ -2768,7 +2772,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :n:`hnf`.
 
 .. note::
- The :math:`\delta` rule only applies to transparent constants (see :ref:`TODO-6.10.1-Opaque`
+ The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies`
  on transparency and opacity).
 
 .. tacn:: cbn
@@ -2906,7 +2910,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This tactic applies to any goal. The argument qualid must denote a
    defined transparent constant or local definition (see
-   :ref:`TODO-1.3.2-Definitions` and :ref:`TODO-6.10.2-Transparent`). The tactic
+   :ref:`TODO-1.3.2-Definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic
    ``unfold`` applies the :math:`\delta` rule to each occurrence of the constant to which
    :n:`@qualid` refers in the current goal and then replaces it with its
    :math:`\beta`:math:`\iota`-normal form.
@@ -2942,7 +2946,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This is variant of :n:`unfold @string` where :n:`@string` gets its
    interpretation from the scope bound to the delimiting key :n:`key`
-   instead of its default interpretation (see :ref:`TODO-12.2.2-Localinterpretationrulesfornotations`).
+   instead of its default interpretation (see :ref:`Localinterpretationrulesfornotations`).
 .. tacv:: unfold {+, qualid_or_string at {+, @num}}
 
    This is the most general form, where :n:`qualid_or_string` is either a
@@ -3389,7 +3393,7 @@ The ``hint_definition`` is one of the following expressions:
 + :n:`Cut @regexp`
 
   .. warning:: these hints currently only apply to typeclass
-               proof search and the ``typeclasses eauto`` tactic (:ref:`TODO-20.6.5-typeclasseseauto`).
+               proof search and the ``typeclasses eauto`` tactic (:ref:`typeclasses-eauto`).
 
   This command can be used to cut the proof-search tree according to a regular
   expression matching paths to be cut. The grammar for regular expressions is
@@ -3521,7 +3525,7 @@ at every moment.
    (left to right). Notice that the rewriting bases are distinct from the ``auto``
    hint bases and thatauto does not take them into account.
 
-   This command is synchronous with the section mechanism (see :ref:`TODO-2.4-Sectionmechanism`):
+   This command is synchronous with the section mechanism (see :ref:`section-mechanism`):
    when closing a section, all aliases created by ``Hint Rewrite`` in that
    section are lost. Conversely, when loading a module, all ``Hint Rewrite``
    declarations at the global level of that module are loaded.
@@ -3592,6 +3596,8 @@ non-imported hints.
    When set, it changes the behavior of an unloaded hint to a immediate fail
    tactic, allowing to emulate an import-scoped hint mechanism.
 
+.. _tactics-implicit-automation:
+
 Setting implicit automation tactics
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -3602,17 +3608,17 @@ Setting implicit automation tactics
    In this case the tactic command typed by the user is equivalent to
    ``tactic``:sub:`1` ``;tactic``.
 
-See also: Proof. in :ref:`TODO-7.1.4-Proofterm`.
+See also: ``Proof.`` in :ref:`proof-editing-mode`.
 
 **Variants:**
 
 .. cmd:: Proof with tactic using {+ @ident}
 
-   Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`TODO-7.1.5-Proofusing`
+   Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
 .. cmd:: Proof using {+ @ident} with tactic
 
-   Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`TODO-7.1.5-Proofusing`
+   Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
 .. cmd:: Declare Implicit Tactic tactic
 
@@ -3878,7 +3884,7 @@ succeeds, and results in an error otherwise.
 .. tacv:: unify @term @term with @ident
 
    Unification takes the transparency information defined in the hint database
-   :n:`@ident` into account (see :ref:`the hints databases for auto and eauto <the-hints-databases-for-auto-and-eauto>`).
+   :n:`@ident` into account (see :ref:`the hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`).
 
 .. tacn:: is_evar @term
    :name: is_evar
@@ -4044,7 +4050,7 @@ 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:`TODO-2.3-advancedrecursivefunctions`). Note that this tactic is only
+:ref:`advanced-recursive-functions`). Note that this tactic is only
 available after a ``Require Import FunInd``.
 
 
@@ -4077,7 +4083,7 @@ This kind of inversion has nothing to do with the tactic :tacn:`inversion`
 above. This tactic does :g:`change (@ident t)`, where `t` is a term built in
 order to ensure the convertibility. In other words, it does inversion of the
 function :n:`@ident`. This function must be a fixpoint on a simple recursive
-datatype: see :ref:`TODO-10.3-quote` for the full details.
+datatype: see :ref:`quote` for the full details.
 
 
 .. exn:: quote: not a simple fixpoint
@@ -4109,6 +4115,8 @@ using the ``Require Import`` command.
    Use ``classical_right`` to prove the right part of the disjunction with
    the assumption that the negation of left part holds.
 
+.. _tactics-automatizing:
+
 Automatizing
 ------------
 
@@ -4148,7 +4156,7 @@ 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:`TODO-21-omega`).
+(see Chapter :ref:`omega`).
 
 
 .. tacn:: ring
@@ -4168,7 +4176,7 @@ 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:`TODO-Chapter-25-Theringandfieldtacticfamilies` for more information on
+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.
 
@@ -4194,7 +4202,7 @@ 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:`TODO-Chapter-25-Theringandfieldtacticfamilies` for more information on the tactic and how to
+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.
 
@@ -4334,7 +4342,7 @@ A simple example has more value than a long explanation:
 
 The tactics macros are synchronous with the Coq section mechanism: a
 tactic definition is deleted from the current environment when you
-close the section (see also :ref:`TODO-2.4Sectionmechanism`) where it was
+close the section (see also :ref:`section-mechanism`) where it was
 defined. If you want that a tactic macro defined in a module is usable in the
 modules that require it, you should put it outside of any section.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 0bb6eea23..f7693d551 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -77,10 +77,11 @@ section.
 Flags, Options and Tables
 -----------------------------
 
-|Coq| configurability is based on flags (e.g. Set Printing All in
-Section :ref:`TODO-2.9-printing-full`), options (e.g. ``Set Printing Widthinteger`` in Section
-:ref:`TODO-6.9.6-set-printing-width`), or tables (e.g. ``Add Printing Record ident``, in Section
-:ref:`TODO-2.2.4-add-printing-record`). The names of flags, options and tables are made of non-empty sequences of identifiers
+|Coq| configurability is based on flags (e.g. ``Set Printing All`` in
+Section :ref:`printing_constructions_full`), options (e.g. ``Set Printing Widthinteger`` in Section
+:ref:`controlling-display`), or tables (e.g. ``Add Printing Record ident``, in Section
+:ref:`record-types`).
+The names of flags, options and tables are made of non-empty sequences of identifiers
 (conventionally with capital initial
 letter). The general commands handling flags, options and tables are
 given below.
@@ -95,7 +96,6 @@ when the current module ends.
 
 Variants:
 
-
 .. cmdv:: Local Set @flag.
 
 This command switches :n:`@flag` on. The original state
@@ -228,7 +228,7 @@ Variants:
 .. cmdv:: @selector: Check @term.
 
 specifies on which subgoal to perform typing
-(see Section :ref:`TODO-8.1-invocation-of-tactics`).
+(see Section :ref:`invocation-of-tactics`).
 
 .. TODO : convtactic is not a syntax entry
 
@@ -240,7 +240,7 @@ hypothesis introduced in the first subgoal (if a proof is in
 progress).
 
 
-See also: Section :ref:`TODO-8.7-performing-computations`.
+See also: Section :ref:`performingcomputations`.
 
 
 .. cmd:: Compute @term.
@@ -250,7 +250,7 @@ bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in``
 :n:`@term`.
 
 
-See also: Section :ref:`TODO-8.7-performing-computations`.
+See also: Section :ref:`performingcomputations`.
 
 
 .. cmd::Extraction @term.
@@ -258,7 +258,7 @@ See also: Section :ref:`TODO-8.7-performing-computations`.
 This command displays the extracted term from :n:`@term`. The extraction is
 processed according to the distinction between ``Set`` and ``Prop``; that is
 to say, between logical and computational content (see Section
-:ref:`TODO-4.1.1-sorts`). The extracted term is displayed in OCaml
+:ref:`sorts`). The extracted term is displayed in OCaml
 syntax,
 where global identifiers are still displayed as in |Coq| terms.
 
@@ -272,7 +272,7 @@ Recursively extracts all
 the material needed for the extraction of the qualified identifiers.
 
 
-See also: Chapter ref:`TODO-23-chapter-extraction`.
+See also: Chapter :ref:`extraction`.
 
 
 .. cmd:: Print Assumptions @qualid.
@@ -326,13 +326,13 @@ 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:`TODO-12.1-notations`), the command works like ``Search`` :n:`@qualid`.
+`"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`.
 
 .. 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:`TODO-12.2.2-local-interpretation-rules-for-notations`).
+the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`).
 
 .. cmdv:: Search @term_pattern.
 
@@ -364,7 +364,7 @@ This restricts the search to constructions not defined in the modules named by t
 .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string.
 
 This specifies the goal on which to search hypothesis (see
-Section :ref:`TODO-8.1-invocation-of-tactics`).
+Section :ref:`invocation-of-tactics`).
 By default the 1st goal is searched. This variant can
 be combined with other variants presented here.
 
@@ -382,11 +382,11 @@ be combined with other variants presented here.
    Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 
 .. 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.
+   ``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.
 
 
 .. cmd:: SearchHead @term.
@@ -420,12 +420,12 @@ Error messages:
 .. exn:: Module/section @qualid not found
 
 No module :n:`@qualid` has been required
-(see Section :ref:`TODO-6.5.1-require`).
+(see Section :ref:`compiled-files`).
 
 .. cmdv:: @selector: SearchHead @term.
 
 This specifies the goal on which to
-search hypothesis (see Section :ref:`TODO-8.1-invocation-of-tactics`).
+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.
@@ -479,7 +479,7 @@ This restricts the search to constructions not defined in the modules named by t
 .. cmdv:: @selector: SearchPattern @term.
 
 This specifies the goal on which to
-search hypothesis (see Section :ref:`TODO-8.1-invocation-of-tactics`). By default the 1st goal is
+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.
 
@@ -514,7 +514,7 @@ This restricts the search to constructions not defined in the modules named by t
 .. cmdv:: @selector: SearchRewrite @term.
 
 This specifies the goal on which to
-search hypothesis (see Section :ref:`TODO-8.1-invocation-of-tactics`). By default the 1st goal is
+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.
 
@@ -569,7 +569,7 @@ As Locate but restricted to modules.
 As Locate but restricted to tactics.
 
 
-See also: Section :ref:`TODO-12.1.10-LocateSymbol`
+See also: Section :ref:`locating-notations`
 
 
 .. _loading-files:
@@ -589,7 +589,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
 
 This command loads the file named :n:`ident`.v, searching successively in
 each of the directories specified in the *loadpath*. (see Section
-:ref:`TODO-2.6.3-libraries-and-filesystem`)
+:ref:`libraries-and-filesystem`)
 
 Files loaded this way cannot leave proofs open, and the ``Load``
 command cannot be used inside a proof either.
@@ -610,7 +610,7 @@ will use the default extension ``.v``.
 
 Display, while loading,
 the answers of |Coq| to each command (including tactics) contained in
-the loaded file See also: Section :ref:`TODO-6.9.1-silent`.
+the loaded file See also: Section :ref:`controlling-display`.
 
 Error messages:
 
@@ -626,7 +626,7 @@ Compiled files
 ------------------
 
 This section describes the commands used to load compiled files (see
-Chapter :ref:`TODO-14-coq-commands` for documentation on how to compile a file). A compiled
+Chapter :ref:`thecoqcommands` for documentation on how to compile a file). A compiled
 file is a particular case of module called *library file*.
 
 
@@ -644,7 +644,7 @@ 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:`TODO-2.6.3-libraries-and-filesystem`). The mapping between
+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.
@@ -656,7 +656,7 @@ Variants:
 
 This loads and declares the module :n:`@qualid`
 and its dependencies then imports the contents of :n:`@qualid` as described
-in Section :ref:`TODO-2.5.8-import`.It does not import the modules on which
+: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
@@ -696,7 +696,7 @@ Error messages:
 
 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:`TODO-2.6.3-libraries-and-filesystem`).
+directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`).
 
 .. exn:: Compiled library ident.vo makes inconsistent assumptions over library qualid
 
@@ -725,12 +725,12 @@ the time it was compiled.
 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:`TODO-2.5.8-import`).
+that the commands ``Import`` and ``Export`` alone can be used inside modules
+(see Section :ref:`Import <import_qualid>`).
 
 
 
-See also: Chapter :ref:`TODO-14-coq-commands`
+See also: Chapter :ref:`thecoqcommands`
 
 
 .. cmd:: Print Libraries.
@@ -746,8 +746,8 @@ 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:`TODO-2.6.3-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:`TODO-14-coq-commands`), or when |Coq| has been compiled with a
+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).
 
 
@@ -774,7 +774,7 @@ Error messages:
 
 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 Section :ref:`TODO-6.6.10-locate-file`)
+should use the command ``Locate File`` (see :ref:`here <locate-file>`)
 
 
 .. _loadpath:
@@ -783,7 +783,7 @@ Loadpath
 ------------
 
 Loadpaths are preferably managed using |Coq| command line options (see
-Section `2.6.3-libraries-and-filesystem`) but there remain vernacular commands to manage them
+Section `libraries-and-filesystem`) but there remain vernacular commands to manage them
 for practical purposes. Such commands are only meant to be issued in
 the toplevel, and using them in source files is discouraged.
 
@@ -862,14 +862,14 @@ the paths that extend the :n:`@dirpath` prefix.
 .. 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:`TODO-6.5-compiled-files`).
+loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
 
 
 .. 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:`TODO-6.5-compiled-files`).
+in Section :ref:`compiled-files`).
 
 
 .. cmd:: Print ML Path @string.
@@ -877,8 +877,9 @@ in Section :ref:`TODO-6.5-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:`TODO-6.5-compiled-files`).
+(see the command Declare ML Module in Section :ref:`compiled-files`).
 
+.. _locate-file:
 
 .. cmd:: Locate File @string.
 
@@ -929,7 +930,7 @@ of the interactive session.
 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:`TODO-7-proof-handling`). For that, Back may have to undo more than
+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
@@ -978,9 +979,9 @@ 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:`TODO-7-proof-handling`).
+      |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:`TODO-7-proof-handling`).
+      opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`).
 
 
 
@@ -1035,10 +1036,10 @@ Warnings:
 
 
 #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`,
-   see Section `TODO-14.1-interactive-use`).
+   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 `14.3.2-customization-by-envionment-variables`).
+   (see Section `customization-by-environment-variables`).
 
 
 
@@ -1108,7 +1109,7 @@ This command turns off the normal displaying.
 
 This command turns the normal display on.
 
-TODO : check that spaces are handled well
+.. todo:: check that spaces are handled well
 
 .. cmd:: Set Warnings ‘‘(@ident {* , @ident } )’’.
 
@@ -1196,7 +1197,7 @@ This command displays the current state of compaction of goal.
 
 This command resets the displaying of goals to focused goals only
 (default). Unfocused goals are created by focusing other goals with
-bullets (see :ref:`TODO-7.2.7-bullets`) or curly braces (see `7.2.6-curly-braces`).
+bullets (see :ref:`bullets`) or curly braces (see `here <curly-braces>`).
 
 
 .. cmd:: Set Printing Unfocused.
@@ -1221,6 +1222,7 @@ when -emacs is passed.
 This command disables the printing of the “(dependent evars: …)” line
 when -emacs is passed.
 
+.. _vernac-controlling-the-reduction-strategies:
 
 Controlling the reduction strategies and the conversion algorithm
 ----------------------------------------------------------------------
@@ -1249,14 +1251,14 @@ 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:`TODO-4.3-conversion-rules`) of two distinct
+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.
 
 
-See also: sections :ref:`TODO-8.7-performing-computations`, :ref:`TODO-8.16-automatizing`, :ref:`TODO-7.1-switching-on-off-proof-editing-mode`
+See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
 
 
 Error messages:
@@ -1294,8 +1296,9 @@ There is no constant referred by :n:`@qualid` in the environment.
 
 
 
-See also: sections :ref:`TODO-8.7-performing-computations`, :ref:`TODO-8.16-automatizing`, :ref:`TODO-7.1-switching-on-off-proof-editing-mode`
+See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
 
+.. _vernac-strategy:
 
 .. cmd:: Strategy @level [ {+ @qualid } ].
 
@@ -1367,7 +1370,7 @@ nothing prevents the user to also perform a
 ``Ltac`` `ident` ``:=`` `convtactic`.
 
 
-See also: sections :ref:`TODO-8.7-performing-computations`
+See also: sections :ref:`performingcomputations`
 
 
 .. _controlling-locality-of-commands:
@@ -1387,8 +1390,8 @@ scope of their effect. There are four kinds of commands:
   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 ``Coercion``
-  (see Section :ref:`TODO-2.8-coercions`) and ``Strategy`` (see Section :ref:`TODO-6.10.3-strategy`) commands belong
-  to this category.
+  (see Section :ref:`coercions`) and ``Strategy`` (see :ref:`here <vernac-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 extent their effect outside the
   module or library file they occur in.  For these commands, the Local
@@ -1396,14 +1399,14 @@ scope of their effect. There are four kinds of commands:
   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 ``Implicit Arguments`` (see
-  Section :ref:`TODO-2.7-implicit-arguments`), Ltac (see Chapter :ref:`TODO-9-tactic-language`) or ``Notation`` (see Section
-  :ref:`TODO-12.1-notations`) commands belong to this category.  Notice that a subclass of
+  Section :ref:`implicitarguments`), Ltac (see Chapter :ref:`TODO-9-tactic-language`) or ``Notation`` (see Section
+  :ref:`notations`) 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 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
-  occurs in.  The ``Transparent`` and ``Opaque`` (see Section :ref:`TODO-6.10-opaque`) commands  belong to this category.
+  occurs in.  The ``Transparent`` and ``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