Merge PR #7252: Sphinx doc fix warnings

6 files changed, 225 insertions, 202 deletions

diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 932f967881..84810ddba5 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
@@ -733,7 +736,7 @@ and this length is decremented for each rotation down to, but not
 including, 1 because for a list of length ``n``, we can make exactly
 ``n−1`` rotations to generate at most ``n`` distinct lists. Here, it
 must be noticed that we use the natural numbers of Coq for the
-rotation counter. On Figure :ref:`TODO-9.1-tactic-language`, we can
+rotation counter. In :ref:`ltac-syntax`, we can
 see that it is possible to use usual natural numbers but they are only
 used as arguments for primitive tactics and they cannot be handled, in
 particular, we cannot make computations with them. So, a natural
@@ -830,7 +833,7 @@ The pattern matching on goals allows a complete and so a powerful
 backtracking when returning tactic values. An interesting application
 is the problem of deciding intuitionistic propositional logic.
 Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff
-:ref:`TODO-56-biblio`, it is quite natural to code such a tactic
+:cite:`Dyc92`, it is quite natural to code such a tactic
 using the tactic language as shown on figures: :ref:`Deciding
 intuitionistic propositions (1) <decidingintuitionistic1>` and
 :ref:`Deciding intuitionistic propositions (2)
@@ -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:`RC95`). The axioms of this λ-calculus are given below.
 
 .. coqtop:: in reset
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 003d4b2438..247d5d899c 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -13,33 +13,34 @@ especially about its foundations, you can refer to :cite:`Del00`. Chapter
 :ref:`detailedexamplesoftactics` is devoted to giving examples of use of this
 language on small but also with non-trivial problems.
 
+.. _ltac-syntax:
+
 Syntax
 ------
 
-The syntax of the tactic language is given Figures :ref:`ltac, ltac_aux`. See
-Chapter :ref:`gallina` for a description of the BNF metasyntax used in these
-grammar rules. Various already defined entries will be used in this chapter:
-entries :token:`natural`, :token:`integer`, :token:`ident`, :token:`qualid`,
-:token:`term`, :token:`cpattern` and :token:`atomic_tactic` represent
-respectively the natural and integer numbers, the authorized identificators and
-qualified names, Coq terms and patterns and all the atomic tactics described in
-Chapter :ref:`tactics`. The syntax of :token:`cpattern` is the same as that of
-terms, but it is extended with pattern matching metavariables. In
-:token:`cpattern`, a pattern-matching metavariable is represented with the
-syntax :g:`?id` where :g:`id` is an :token:`ident`. The notation :g:`_` can also
-be used to denote metavariable whose instance is irrelevant. In the notation
-:g:`?id`, the identifier allows us to keep instantiations and to make
-constraints whereas :g:`_` shows that we are not interested in what will be
-matched. On the right hand side of pattern-matching clauses, the named
-metavariable are used without the question mark prefix. There is also a special
-notation for second-order pattern-matching problems: in an applicative pattern
-of the form :g:`@?id id1 … idn`, the variable id matches any complex expression
-with (possible) dependencies in the variables :g:`id1 … idn` and returns a
-functional term of the form :g:`fun id1 … idn => term`.
+The syntax of the tactic language is given below. See Chapter
+:ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used
+in these grammar rules. Various already defined entries will be used in this
+chapter: entries :token:`natural`, :token:`integer`, :token:`ident`,
+:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`atomic_tactic`
+represent respectively the natural and integer numbers, the authorized
+identificators and qualified names, Coq terms and patterns and all the atomic
+tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is
+the same as that of terms, but it is extended with pattern matching
+metavariables. In :token:`cpattern`, a pattern-matching metavariable is
+represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The
+notation :g:`_` can also be used to denote metavariable whose instance is
+irrelevant. In the notation :g:`?id`, the identifier allows us to keep
+instantiations and to make constraints whereas :g:`_` shows that we are not
+interested in what will be matched. On the right hand side of pattern-matching
+clauses, the named metavariable are used without the question mark prefix. There
+is also a special notation for second-order pattern-matching problems: in an
+applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any
+complex expression with (possible) dependencies in the variables :g:`id1 … idn`
+and returns a functional term of the form :g:`fun id1 … idn => term`.
 
 The main entry of the grammar is :n:`@expr`. This language is used in proof
-mode but it can also be used in toplevel definitions as shown in
-Figure :ref:`ltactop`.
+mode but it can also be used in toplevel definitions as shown below.
 
 .. note::
 
@@ -153,6 +154,8 @@ Figure :ref:`ltactop`.
    ltac_def         : `ident` [`ident` ... `ident`] := `expr`
                     : | `qualid` [`ident` ... `ident`] ::= `expr`
 
+.. _ltac-semantics:
+
 Semantics
 ---------
 
@@ -228,6 +231,8 @@ following form:
       independently. All the above variants work in this form too.
       Formally, :n:`@expr ; [ ... ]` is equivalent to :n:`[> @expr ; [> ... ] .. ]`.
 
+.. _goal-selectors:
+
 Goal selectors
 ~~~~~~~~~~~~~~
 
@@ -247,7 +252,7 @@ focused goals with:
    .. tacv:: [@ident] : @expr
 
       In this variant, :n:`@expr` is applied locally to a goal previously named
-      by the user (see :ref:`ExistentialVariables`).
+      by the user (see :ref:`existential-variables`).
 
    .. tacv:: @num : @expr
 
@@ -275,6 +280,9 @@ focused goals with:
       the toplevel of a tactic expression.
 
    .. exn:: No such goal
+      :name: No such goal (goal selector)
+
+   .. TODO change error message index entry
 
 For loop
 ~~~~~~~~
@@ -759,7 +767,7 @@ We can carry out pattern matching on terms with:
       matching subterm is tried. If no further subterm matches, the next clause
       is tried. Matching subterms are considered top-bottom and from left to
       right (with respect to the raw printing obtained by setting option
-      ``Printing All``, see Section :ref:`SetPrintingAll`).
+      :opt:`Printing All`).
 
    .. example::
 
@@ -775,6 +783,8 @@ We can carry out pattern matching on terms with:
          Goal True.
          f (3+4).
 
+.. _ltac-match-goal:
+
 Pattern matching on goals
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1009,6 +1019,7 @@ Proving a subgoal as a separate lemma
          don’t play well with asynchronous proofs.
 
    .. exn:: Proof is not complete
+      :name: Proof is not complete (abstract)
 
 Tactic toplevel definitions
 ---------------------------
@@ -1253,4 +1264,4 @@ Run-time optimization tactic
 
 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 ``Optimize Heap`` (see :ref:`vernac-optimizeheap`).
+command :cmd:`Optimize Heap`.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index adf3da3ebb..a77b127ebe 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -20,20 +20,18 @@ prove. Initially, the list consists only in the theorem itself. After
 having applied some tactics, the list of goals contains the subgoals
 generated by the tactics.
 
-To each subgoal is associated a number of hypotheses called the *local
-context* of the goal. Initially, the local context contains the local
-variables and hypotheses of the current section (see Section :ref:`TODO_gallina_assumptions`)
-and the local variables and hypotheses of the theorem statement. It is
-enriched by the use of certain tactics (see e.g. ``intro`` in Section
-:ref:`managingthelocalcontext`).
+To each subgoal is associated a number of hypotheses called the *local context*
+of the goal. Initially, the local context contains the local variables and
+hypotheses of the current section (see Section :ref:`gallina-assumptions`) and
+the local variables and hypotheses of the theorem statement. It is enriched by
+the use of certain tactics (see e.g. :tacn:`intro`).
 
 When a proof is completed, the message ``Proof completed`` is displayed.
 One can then register this proof as a defined constant in the
 environment. Because there exists a correspondence between proofs and
-terms of λ-calculus, known as the *Curry-Howard isomorphism* [[How80]_,
-[Bar81]_, [Gir89]_, [Hue88]_ ], |Coq|
-stores proofs as terms of |Cic|. Those terms
-are called *proof terms*.
+terms of λ-calculus, known as the *Curry-Howard isomorphism*
+:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those
+terms are called *proof terms*.
 
 
 .. exn:: No focused proof
@@ -41,16 +39,15 @@ 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
 -------------------------------------------
 
-The proof editing mode is entered by asserting a statement, which
-typically is the assertion of a theorem:
-
-.. cmd:: Theorem @ident [@binders] : @form.
-
-The list of assertion commands is given in Section :ref:TODO-assertions_and_proof`. The
-command ``Goal`` can also be used.
+The proof editing mode is entered by asserting a statement, which typically is
+the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
+list of assertion commands is given in Section :ref:`Assertions`. The command
+:cmd:`Goal` can also be used.
 
 .. cmd:: Goal @form.
 
@@ -93,14 +90,13 @@ Forces the name of the original goal to be :n:`@ident`. This
 command (and the following ones) can only be used if the original goal
 has been opened using the ``Goal`` command.
 
-
 .. cmd:: Admitted.
 
 This command is available in interactive editing proof mode to give up
 the current proof and declare the initial goal as an axiom.
 
-
 .. cmd:: Proof @term.
+   :name: Proof `term`
 
 This command applies in proof editing mode. It is equivalent to
 
@@ -119,13 +115,13 @@ closing ``Qed``.
 
 
 See also: ``Proof with tactic.`` in Section
-:ref:`setimpautotactics`.
+:ref:`tactics-implicit-automation`.
 
 
 .. cmd:: Proof using @ident1 ... @identn.
 
 This command applies in proof editing mode. It declares the set of
-section variables (see :ref:`TODO-gallina-assumptions`) used by the proof. At ``Qed`` time, the
+section variables (see :ref:`gallina-assumptions`) used by the proof. At ``Qed`` time, the
 system will assert that the set of section variables actually used in
 the proof is a subset of the declared one.
 
@@ -136,7 +132,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 +258,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 +323,7 @@ last ``Focus`` command.
 Succeeds if the proof is fully unfocused, fails is there are some
 goals out of focus.
 
+.. _curly-braces:
 
 .. cmd:: %{ %| %}
 
@@ -351,12 +348,14 @@ Error messages:
 You are trying to use ``}`` but the current subproof has not been fully solved.
 
 .. exn:: No such goal
+   :name: No such goal (focusing)
 
 .. exn:: Brackets only support the single numbered goal selector
 
-
 See also error messages about bullets below.
 
+.. _bullets:
+
 Bullets
 ```````
 
@@ -434,6 +433,7 @@ This makes bullets inactive.
 This makes bullets active (this is the default behavior).
 
 
+.. _requestinginformation:
 
 Requesting information
 ----------------------
@@ -456,7 +456,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 +536,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
@@ -591,4 +591,4 @@ the ongoing proof.
 This command forces the |OCaml| runtime to perform a heap compaction.
 This is in general an expensive operation.
 See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-There is also an analogous tactic ``optimize_heap`` (see~:ref:`tactic-optimizeheap`)
+There is also an analogous tactic :tac:`optimize_heap`.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index df5b362970..074c6f1e28 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5185,6 +5185,7 @@ equivalences are indeed taken into account, otherwise only single
 |SSR| proposes an extension of the Search command. Its syntax is:
 
 .. cmd:: Search {? @pattern }  {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } }
+   :name: Search (ssreflect)
 
 where :token:`qualid` is the name of an open module. This command returns
 the list of lemmas:
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2af73c28e5..08aa7110d1 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
@@ -34,15 +34,16 @@ satisfied. If it is not the case, the tactic raises an error message.
 Tactics are built from atomic tactics and tactic expressions (which
 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`.
+language will be described in Chapter :ref:`ltac`.
+
+.. _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.
+goal selector (see Section :ref:`ltac-semantics`). If no selector is
+specified, the default selector is used.
 
 .. _tactic_invocation_grammar:
 
@@ -94,7 +95,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
 + A bindings list can also be a simple list of terms :n:`{* term}`.
   In that case the references to which these terms correspond are
   determined by the tactic. In case of ``induction``, ``destruct``, ``elim``
-  and ``case`` (see :ref:`TODO-9-Thetacticlanguage`) the terms have to
+  and ``case`` (see :ref:`ltac`) the terms have to
   provide instances for all the dependent products in the type of term while in
   the case of ``apply``, or of ``constructor`` and its variants, only instances
   for the dependent products that are not bound in the conclusion of the type
@@ -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.
 
@@ -277,7 +279,7 @@ gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...`  :g:`u`:sub:`n`.
 
 The apply tactic failed to match the conclusion of term and the current goal.
 You can help the apply tactic by transforming your goal with the
-:ref:`change <change_term>` or :tacn:`pattern` tactics.
+:tacn:`change` or :tacn:`pattern` tactics.
 
 .. exn:: Unable to find an instance for the variables {+ @ident}.
 
@@ -285,7 +287,7 @@ This occurs when some instantiations of the premises of term are not deducible
 from the unification. This is the case, for instance, when you want to apply a
 transitivity property. In this case, you have to use one of the variants below:
 
-.. cmd:: apply @term with {+ @term}
+.. tacv:: apply @term with {+ @term}
 
 Provides apply with explicit instantiations for all dependent premises of the
 type of term that do not occur in the conclusion and consequently cannot be
@@ -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:
 
@@ -1089,7 +1091,7 @@ Controlling the proof flow
 
 .. tacv:: assert form
 
-   This behaves as :n:`assert (@ident : form ) but :n:`@ident` is generated by
+   This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by
    Coq.
 
 .. tacv:: assert form by tactic
@@ -1098,6 +1100,7 @@ Controlling the proof flow
    generated by assert.
 
    .. exn:: Proof is not complete
+      :name: Proof is not complete (assert)
 
 .. tacv:: assert form as intro_pattern
 
@@ -1177,7 +1180,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 +1271,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 +1356,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 +1751,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 the larger example of :tacn:`dependent induction`
 and an explanation of the underlying technique.
 
 .. tacn:: function induction (@qualid {+ @term})
@@ -1754,8 +1759,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 +1786,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 +1907,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 +1989,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 +2305,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 +2326,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 +2340,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 +2551,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 +2569,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 +2642,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 +2654,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 +2773,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 +2911,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:`gallina-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 +2947,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 +3394,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 +3526,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 +3597,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,40 +3609,37 @@ 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`.
-
-**Variants:**
+   See also: ``Proof.`` in :ref:`proof-editing-mode`.
 
-.. cmd:: Proof with tactic using {+ @ident}
 
-   Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`TODO-7.1.5-Proofusing`
+   .. cmdv:: Proof with tactic using {+ @ident}
 
-.. cmd:: Proof using {+ @ident} with tactic
+      Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
-   Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`TODO-7.1.5-Proofusing`
+   .. cmdv:: Proof using {+ @ident} with tactic
 
-.. cmd:: Declare Implicit Tactic tactic
+      Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
-   This command declares a tactic to be used to solve implicit arguments
-   that Coq does not know how to solve by unification. It is used every
-   time the term argument of a tactic has one of its holes not fully
-   resolved.
+   .. cmd:: Declare Implicit Tactic tactic
 
-Here is an example:
+      This command declares a tactic to be used to solve implicit arguments
+      that Coq does not know how to solve by unification. It is used every
+      time the term argument of a tactic has one of its holes not fully
+      resolved.
 
-.. example::
+   .. example::
 
-   .. coqtop:: all
+      .. coqtop:: all
 
-      Parameter quo : nat -> forall n:nat, n<>0 -> nat.
-      Notation "x // y" := (quo x y _) (at level 40).
-      Declare Implicit Tactic assumption.
-      Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
-      intros.
-      exists (n // m).
+         Parameter quo : nat -> forall n:nat, n<>0 -> nat.
+         Notation "x // y" := (quo x y _) (at level 40).
+         Declare Implicit Tactic assumption.
+         Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
+         intros.
+         exists (n // m).
 
-   The tactic ``exists (n // m)`` did not fail. The hole was solved
-   by ``assumption`` so that it behaved as ``exists (quo n m H)``.
+      The tactic ``exists (n // m)`` did not fail. The hole was solved
+      by ``assumption`` so that it behaved as ``exists (quo n m H)``.
 
 .. _decisionprocedures:
 
@@ -3713,7 +3717,7 @@ 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
-mainly the tactic language (see :ref:`TODO-9-thetacticlanguage`). The code is
+mainly the tactic language (see :ref:`ltac`). The code is
 now much shorter and a significant increase in performance has been noticed.
 The general behavior with respect to dependent types, unfolding and
 introductions has slightly changed to get clearer semantics. This may lead to
@@ -3878,7 +3882,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 +4048,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 +4081,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 +4113,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 +4154,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 +4174,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 +4200,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,11 +4340,11 @@ 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.
 
-:ref:`TODO-9-Thetacticlanguage` gives examples of more complex
+:ref:`ltac` gives examples of more complex
 user-defined tactics.
 
 .. [1] Actually, only the second subgoal will be generated since the
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 0bb6eea233..da4034fb8a 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,23 +1390,22 @@ 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
-  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 ``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
-  these commands do not support extension of their scope outside
-  sections at all and the Global is not applicable to them.
+  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 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:`Implicit 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 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