[sphinx] Fix many warnings.

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

22 files changed, 398 insertions, 345 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index d7f97edab..38365e403 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -1,16 +1,16 @@
-.. _extraction:
-
 .. include:: ../replaces.rst
 
-Extraction of programs in OCaml and Haskell
-============================================
+.. _extraction:
+
+Extraction of programs in |OCaml| and Haskell
+=============================================
 
 :Authors: Jean-Christophe Filliâtre and Pierre Letouzey
 
 We present here the |Coq| extraction commands, used to build certified
 and relatively efficient functional programs, extracting them from
 either |Coq| functions or |Coq| proofs of specifications. The
-functional languages available as output are currently OCaml, Haskell
+functional languages available as output are currently |OCaml|, Haskell
 and Scheme. In the following, "ML" will be used (abusively) to refer
 to any of the three.
 
@@ -89,11 +89,11 @@ in the |Coq| sources.
 .. cmd:: Extraction TestCompile @qualid ... @qualid.
 
    All the mentioned objects and all their dependencies are extracted
-   to a temporary OCaml file, just as in ``Extraction "file"``. Then
+   to a temporary |OCaml| file, just as in ``Extraction "file"``. Then
    this temporary file and its signature are compiled with the same
-   OCaml compiler used to built |Coq|. This command succeeds only
-   if the extraction and the OCaml compilation succeed. It fails
-   if the current target language of the extraction is not OCaml.
+   |OCaml| compiler used to built |Coq|. This command succeeds only
+   if the extraction and the |OCaml| compilation succeed. It fails
+   if the current target language of the extraction is not |OCaml|.
 
 Extraction Options
 -------------------
@@ -102,26 +102,26 @@ Setting the target language
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The ability to fix target language is the first and more important
-of the extraction options. Default is ``Ocaml``.
+of the extraction options. Default is ``OCaml``.
 
-.. cmd:: Extraction Language Ocaml.
+.. cmd:: Extraction Language OCaml.
 .. cmd:: Extraction Language Haskell.
 .. cmd:: Extraction Language Scheme.
 
 Inlining and optimizations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Since OCaml is a strict language, the extracted code has to
+Since |OCaml| is a strict language, the extracted code has to
 be optimized in order to be efficient (for instance, when using
 induction principles we do not want to compute all the recursive calls
 but only the needed ones). So the extraction mechanism provides an
 automatic optimization routine that will be called each time the user
-want to generate OCaml programs. The optimizations can be split in two
+want to generate |OCaml| programs. The optimizations can be split in two
 groups: the type-preserving ones (essentially constant inlining and
 reductions) and the non type-preserving ones (some function
 abstractions of dummy types are removed when it is deemed safe in order
 to have more elegant types). Therefore some constants may not appear in the
-resulting monolithic OCaml program. In the case of modular extraction,
+resulting monolithic |OCaml| program. In the case of modular extraction,
 even if some inlining is done, the inlined constant are nevertheless
 printed, to ensure session-independent programs.
 
@@ -264,10 +264,9 @@ what ML term corresponds to a given axiom.
    be inlined everywhere instead of being declared via a ``let``.
 
    .. note::
-
-   This command is sugar for an ``Extract Constant`` followed
-   by a ``Extraction Inline``. Hence a ``Reset Extraction Inline``
-   will have an effect on the realized and inlined axiom.
+      This command is sugar for an ``Extract Constant`` followed
+      by a ``Extraction Inline``. Hence a ``Reset Extraction Inline``
+      will have an effect on the realized and inlined axiom.
 
 .. caution:: It is the responsibility of the user to ensure that the ML
    terms given to realize the axioms do have the expected types. In
@@ -336,7 +335,7 @@ native boolean type instead of |Coq| one. The syntax is the following:
    argument is considered to have one unit argument, in order to block
    early evaluation of the branch: ``| O => bar`` leads to the functional
    form ``(fun () -> bar)``. For instance, when extracting ``nat``
-   into OCaml ``int``, the code to provide has type:
+   into |OCaml| ``int``, the code to provide has type:
    ``(unit->'a)->(int->'a)->int->'a``.
 
 .. caution:: As for ``Extract Constant``, this command should be used with care:
@@ -347,15 +346,15 @@ native boolean type instead of |Coq| one. The syntax is the following:
   * Extracting an inductive type to a pre-existing ML inductive type
     is quite sound. But extracting to a general type (by providing an
     ad-hoc pattern-matching) will often **not** be fully rigorously
-    correct. For instance, when extracting ``nat`` to OCaml ``int``,
+    correct. For instance, when extracting ``nat`` to |OCaml| ``int``,
     it is theoretically possible to build ``nat`` values that are
-    larger than OCaml ``max_int``. It is the user's responsibility to
+    larger than |OCaml| ``max_int``. It is the user's responsibility to
     be sure that no overflow or other bad events occur in practice.
 
   * Translating an inductive type to an arbitrary ML type does **not**
     magically improve the asymptotic complexity of functions, even if the
     ML type is an efficient representation. For instance, when extracting
-    ``nat`` to OCaml ``int``, the function ``Nat.mul`` stays quadratic.
+    ``nat`` to |OCaml| ``int``, the function ``Nat.mul`` stays quadratic.
     It might be interesting to associate this translation with
     some specific ``Extract Constant`` when primitive counterparts exist.
 
@@ -369,9 +368,9 @@ Typical examples are the following:
 
 .. note::
 
-   When extracting to Ocaml, if an inductive constructor or type has arity 2 and
+   When extracting to |OCaml|, if an inductive constructor or type has arity 2 and
    the corresponding string is enclosed by parentheses, and the string meets
-   Ocaml's lexical criteria for an infix symbol, then the rest of the string is
+   |OCaml|'s lexical criteria for an infix symbol, then the rest of the string is
    used as infix constructor or type.
 
 .. coqtop:: in
@@ -380,7 +379,7 @@ Typical examples are the following:
    Extract Inductive prod => "(*)"  [ "(,)" ].
 
 As an example of translation to a non-inductive datatype, let's turn
-``nat`` into OCaml ``int`` (see caveat above):
+``nat`` into |OCaml| ``int`` (see caveat above):
 
 .. coqtop:: in
 
@@ -394,7 +393,7 @@ directly depends from the names of the |Coq| files. It may happen that
 these filenames are in conflict with already existing files, 
 either in the standard library of the target language or in other
 code that is meant to be linked with the extracted code. 
-For instance the module ``List`` exists both in |Coq| and in OCaml.
+For instance the module ``List`` exists both in |Coq| and in |OCaml|.
 It is possible to instruct the extraction not to use particular filenames.
 
 .. cmd:: Extraction Blacklist @ident ... @ident.
@@ -410,7 +409,7 @@ It is possible to instruct the extraction not to use particular filenames.
 
    Allow the extraction to use any filename.
 
-For OCaml, a typical use of these commands is
+For |OCaml|, a typical use of these commands is
 ``Extraction Blacklist String List``.
 
 Differences between |Coq| and ML type systems
@@ -418,7 +417,7 @@ Differences between |Coq| and ML type systems
 
 Due to differences between |Coq| and ML type systems, 
 some extracted programs are not directly typable in ML. 
-We now solve this problem (at least in OCaml) by adding 
+We now solve this problem (at least in |OCaml|) by adding
 when needed some unsafe casting ``Obj.magic``, which give
 a generic type ``'a`` to any term.
 
@@ -432,7 +431,7 @@ function:
 
    Definition dp {A B:Type}(x:A)(y:B)(f:forall C:Type, C->C) := (f A x, f B y).
 
-In Ocaml, for instance, the direct extracted term would be::
+In |OCaml|, for instance, the direct extracted term would be::
 
    let dp x y f = Pair((f () x),(f () y))
 
@@ -455,12 +454,12 @@ of a constructor; for example:
    Inductive anything : Type := dummy : forall A:Set, A -> anything.
 
 which corresponds to the definition of an ML dynamic type.
-In OCaml, we must cast any argument of the constructor dummy
+In |OCaml|, we must cast any argument of the constructor dummy
 (no GADT are produced yet by the extraction).
 
 Even with those unsafe castings, you should never get error like
 ``segmentation fault``. In fact even if your program may seem
-ill-typed to the Ocaml type-checker, it can't go wrong : it comes 
+ill-typed to the |OCaml| type-checker, it can't go wrong : it comes
 from a Coq well-typed terms, so for example inductive types will always 
 have the correct number of arguments, etc. Of course, when launching
 manually some extracted function, you should apply it to arguments
@@ -470,14 +469,14 @@ More details about the correctness of the extracted programs can be
 found in :cite:`Let02`.
 
 We have to say, though, that in most "realistic" programs, these problems do not
-occur. For example all the programs of Coq library are accepted by the OCaml
+occur. For example all the programs of Coq library are accepted by the |OCaml|
 type-checker without any ``Obj.magic`` (see examples below).
 
 Some examples
 -------------
 
 We present here two examples of extractions, taken from the 
-|Coq| Standard Library. We choose OCaml as target language, 
+|Coq| Standard Library. We choose |OCaml| as target language,
 but all can be done in the other dialects with slight modifications.
 We then indicate where to find other examples and tests of extraction.
 
@@ -493,7 +492,7 @@ This module contains a theorem ``eucl_dev``, whose type is::
 
 where ``diveucl`` is a type for the pair of the quotient and the
 modulo, plus some logical assertions that disappear during extraction.
-We can now extract this program to OCaml:
+We can now extract this program to |OCaml|:
 
 .. coqtop:: none
 
@@ -513,7 +512,7 @@ You can then copy-paste the output to a file ``euclid.ml`` or let
 
    Extraction "euclid" eucl_dev.
 
-Let us play the resulting program (in an OCaml toplevel)::
+Let us play the resulting program (in an |OCaml| toplevel)::
 
    #use "euclid.ml";;
    type nat = O | S of nat
@@ -527,7 +526,7 @@ Let us play the resulting program (in an OCaml toplevel)::
    # eucl_dev (S (S O)) (S (S (S (S (S O)))));;
    - : diveucl = Divex (S (S O), S O)
 
-It is easier to test on OCaml integers::
+It is easier to test on |OCaml| integers::
 
    # let rec nat_of_int = function 0 -> O | n -> S (nat_of_int (n-1));;
    val nat_of_int : int -> nat = <fun>
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index da9e97e6f..0e72c996f 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -1,14 +1,12 @@
-.. _generalizedrewriting:
-
------------------------
- Generalized rewriting
------------------------
+.. include:: ../preamble.rst
+.. include:: ../replaces.rst
 
-:Author: Matthieu Sozeau
+.. _generalizedrewriting:
 
 Generalized rewriting
 =====================
 
+:Author: Matthieu Sozeau
 
 This chapter presents the extension of several equality related
 tactics to work over user-defined structures (called setoids) that are
@@ -479,7 +477,7 @@ The declaration itself amounts to the definition of an object of the
 record type ``Coq.Classes.RelationClasses.Equivalence`` and a hint added
 to the ``typeclass_instances`` hint database. Morphism declarations are
 also instances of a type class defined in ``Classes.Morphisms``. See the
-documentation on type classes :ref:`TODO-chapter-20-type-classes`
+documentation on type classes :ref:`typeclasses`
 and the theories files in Classes for further explanations.
 
 One can inform the rewrite tactic about morphisms and relations just
@@ -707,7 +705,7 @@ defined constants as transparent by default. This may slow down the
 resolution due to a lot of unifications (all the declared ``Proper``
 instances are tried at each node of the search tree). To speed it up,
 declare your constant as rigid for proof search using the command
-``Typeclasses Opaque`` (see :ref:`TODO-20.6.7-typeclasses-transparency`).
+``Typeclasses Opaque`` (see :ref:`TypeclassesTransparent`).
 
 
 Strategies for rewriting
@@ -812,7 +810,7 @@ Hint databases created for ``autorewrite`` can also be used
 by ``rewrite_strat`` using the ``hints`` strategy that applies any of the
 lemmas at the current subterm. The ``terms`` strategy takes the lemma
 names directly as arguments. The ``eval`` strategy expects a reduction
-expression (see :ref:`TODO-8.7-performing-computations`) and succeeds
+expression (see :ref:`performingcomputations`) and succeeds
 if it reduces the subterm under consideration. The ``fold`` strategy takes
 a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c``
 on success, it is stronger than the tactic ``fold``.
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index f5ca5be44..68e071d7c 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -1,7 +1,7 @@
-.. _implicitcoercions:
-
 .. include:: ../replaces.rst
 
+.. _implicitcoercions:
+
 Implicit Coercions
 ====================
 
@@ -166,7 +166,7 @@ Declaration of Coercions
 
 Assumptions can be declared as coercions at declaration time.
 This extends the grammar of assumptions from
-Figure :ref:`TODO-1.3-sentences-syntax` as follows:
+Figure :ref:`vernacular` as follows:
 
 ..
   FIXME:
@@ -186,7 +186,7 @@ assumptions are declared as coercions.
 
 Similarly, constructors of inductive types can be declared as coercions at
 definition time of the inductive type. This extends and modifies the
-grammar of inductive types from Figure :ref:`TODO-1.3-sentences-syntax` as follows:
+grammar of inductive types from Figure :ref:`vernacular` as follows:
 
 ..
   FIXME:
@@ -267,13 +267,14 @@ Activating the Printing of Coercions
   To skip the printing of coercion `qualid`, use
   ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed.
 
+.. _coercions-classes-as-records:
 
 Classes as Records
 ------------------
 
 We allow the definition of *Structures with Inheritance* (or
 classes as records) by extending the existing ``Record`` macro
-(see Section :ref:`TODO-2.1-Record`). Its new syntax is:
+(see Section :ref:`record-types`). Its new syntax is:
 
 .. cmd:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
 
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 3ed4ce762..80ea8a116 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -3,15 +3,10 @@
 .. _miscellaneousextensions:
 
 Miscellaneous extensions
-=======================
-
-.. contents::
-   :local:
-   :depth: 1
-----
+========================
 
 Program derivation
------------------
+------------------
 
 |Coq| comes with an extension called ``Derive``, which supports program
 derivation. Typically in the style of Bird and Meertens or derivations
@@ -25,7 +20,7 @@ The first `ident` can appear in `term`. This command opens a new proof
 presenting the user with a goal for term in which the name `ident` is
 bound to an existential variable `?x` (formally, there are other goals
 standing for the existential variables but they are shelved, as
-described in Section :ref:`TODO-8.17.4`).
+described in :tacn:`shelve`).
 
 When the proof ends two constants are defined:
 
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index ef9b3505d..387d61495 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -19,7 +19,7 @@ where :math:`P, Q, P₁,Q₁,\ldots,Pₛ, Qₛ` are polynomials and :math:`A` is
 domain, i.e. a commutative ring with no zero divisor. For example, :math:`A`
 can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`.
 Note that the equality :math:`=` used in these goals can be
-any setoid equality (see :ref:`TODO-27.2.2`) , not only Leibnitz equality.
+any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibnitz equality.
 
 It also proves formulas
 
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index 8c1b9d152..edb8676a5 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -39,14 +39,14 @@ Proof annotations
 To process a proof asynchronously |Coq| needs to know the precise
 statement of the theorem without looking at the proof. This requires
 some annotations if the theorem is proved inside a Section (see
-Section :ref:`TODO-2.4`).
+Section :ref:`section-mechanism`).
 
 When a section ends, |Coq| looks at the proof object to decide which
 section variables are actually used and hence have to be quantified in
 the statement of the theorem. To avoid making the construction of
 proofs mandatory when ending a section, one can start each proof with
-the ``Proof using`` command (Section :ref:`TODO-7.1.5`) that declares which section
-variables the theorem uses.
+the ``Proof using`` command (Section :ref:`proof-editing-mode`) that
+declares which section variables the theorem uses.
 
 The presence of ``Proof`` using is needed to process proofs asynchronously
 in interactive mode.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index eb50e52dc..a2940881d 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -135,7 +135,8 @@ support types, avoiding uses of proof-irrelevance that would come up
 when reasoning with equality on the subset types themselves.
 
 The next two commands are similar to their standard counterparts
-Definition (see Section `TODO-1.3.2-Definition`_) and Fixpoint (see Section `TODO-1.3.4-Fixpoint`_)
+Definition (see Section :ref:`gallina_def`) and Fixpoint
+(see Section :ref:`TODO-1.3.4-Fixpoint`)
 in that they define constants. However, they may require the user to
 prove some goals to construct the final definitions.
 
@@ -174,7 +175,7 @@ Program Definition
 
       .. TODO refer to production in alias
 
-See also: Sections `TODO-6.10.1-Opaque`_, `TODO-6.10.2-Transparent`_, `TODO-8.7.5-unfold`_
+See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold`
 
 .. _program_fixpoint:
 
@@ -196,7 +197,7 @@ The optional order annotation follows the grammar:
 + :g:`wf R x` which is equivalent to :g:`measure x (R)`.
 
 The structural fixpoint operator behaves just like the one of |Coq| (see
-Section `TODO-1.3.4-Fixpoint`_), except it may also generate obligations. It works
+Section :ref:`TODO-1.3.4-Fixpoint`), except it may also generate obligations. It works
 with mutually recursive definitions too.
 
 .. coqtop:: reset none
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 5518da9ac..add03b946 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -333,7 +333,7 @@ Variants:
 
 .. cmd:: Program Instance
 
-   Switches the type-checking to Program (chapter :ref:`program`) and
+   Switches the type-checking to Program (chapter :ref:`programs`) and
    uses the obligation mechanism to manage missing fields.
 
 .. cmd:: Declare Instance
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 13d20d7cf..839f3ce56 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -97,7 +97,7 @@ ensure the existence of a mapping of the universes to the positive
 integers, the graph of constraints must remain acyclic. Typing
 expressions that violate the acyclicity of the graph of constraints
 results in a Universe inconsistency error (see also Section
-:ref:`TODO-2.10`).
+:ref:`printing-universes`).
 
 
 .. _Terms:
@@ -709,8 +709,6 @@ called the *context of parameters*. Furthermore, we must have that
 each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{\mathit{Arr}(t)}, S` where
 :math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type t and :math:`S` is called
 the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts).
-
-
 ** Examples** The declaration for parameterized lists is:
 
 .. math::
@@ -1058,7 +1056,7 @@ provided that the following side conditions hold:
       we have :math:`(E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}` ;
     + the sorts :math:`s_i` are such that all eliminations, to
       :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, are allowed
-      (see Section Destructors_).
+      (see Section :ref:`Destructors`).
 
 
 
@@ -1088,14 +1086,14 @@ The sorts :math:`s_j` are chosen canonically so that each :math:`s_j` is minimal
 respect to the hierarchy :math:`\Prop ⊂ \Set_p ⊂ \Type` where :math:`\Set_p` is predicative
 :math:`\Set`. More precisely, an empty or small singleton inductive definition
 (i.e. an inductive definition of which all inductive types are
-singleton – see paragraph Destructors_) is set in :math:`\Prop`, a small non-singleton
+singleton – see Section :ref:`Destructors`) is set in :math:`\Prop`, a small non-singleton
 inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicative – see
 Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_),
 and otherwise in the Type hierarchy.
 
 Note that the side-condition about allowed elimination sorts in the
 rule **Ind-Family** is just to avoid to recompute the allowed elimination
-sorts at each instance of a pattern-matching (see section Destructors_). As
+sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). As
 an example, let us consider the following definition:
 
 .. example::
@@ -1111,7 +1109,7 @@ in the Type hierarchy. Here, the parameter :math:`A` has this property, hence,
 if :g:`option` is applied to a type in :math:`\Set`, the result is in :math:`\Set`. Note that
 if :g:`option` is applied to a type in :math:`\Prop`, then, the result is not set in
 :math:`\Prop` but in :math:`\Set` still. This is because :g:`option` is not a singleton type
-(see section Destructors_) and it would lose the elimination to :math:`\Set` and :math:`\Type`
+(see Section :ref:`Destructors`) and it would lose the elimination to :math:`\Set` and :math:`\Type`
 if set in :math:`\Prop`.
 
 .. example::
@@ -1278,7 +1276,7 @@ and :math:`I:A` and :math:`λ a x . P : B` then by :math:`[I:A|B]` we mean that
 :math:`λ a x . P` with :math:`m` in the above match-construct.
 
 
-.. _Notations:
+.. _cic_notations:
 
 **Notations.** The :math:`[I:A|B]` is defined as the smallest relation satisfying the
 following rules: We write :math:`[I|B]` for :math:`[I:A|B]` where :math:`A` is the type of :math:`I`.
@@ -1684,7 +1682,7 @@ possible:
 **Mutual induction**
 
 The principles of mutual induction can be automatically generated
-using the Scheme command described in Section :ref:`TODO-13.1`.
+using the Scheme command described in Section :ref:`proofschemes-induction-principles`.
 
 
 .. _Admissible-rules-for-global-environments:
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 82ced65b4..c5da866b8 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -19,7 +19,7 @@ The |Coq| library is structured into two parts:
     developments of |Coq| axiomatizations about sets, lists, sorting,
     arithmetic, etc. This library comes with the system and its modules
     are directly accessible through the ``Require`` command (see
-    Section :ref:`TODO-6.5.1-Require`);
+    Section :ref:`compiled-files`);
 
 In addition, user-provided libraries or developments are provided by
 |Coq| users' community. These libraries and developments are available
@@ -90,6 +90,8 @@ Notation          Precedence    Associativity
 ``_ ^ _``         30            right
 ================  ============  ===============
 
+.. _coq-library-logic:
+
 Logic
 ~~~~~
 
@@ -521,7 +523,7 @@ provides a scope ``nat_scope`` gathering standard notations for
 common operations (``+``, ``*``) and a decimal notation for
 numbers, allowing for instance to write ``3`` for :g:`S (S (S O)))`. This also works on
 the left hand side of a ``match`` expression (see for example
-section :ref:`TODO-refine-example`). This scope is opened by default.
+section :tacn:`refine`). This scope is opened by default.
 
 .. example::
 
@@ -753,7 +755,7 @@ subdirectories:
 These directories belong to the initial load path of the system, and
 the modules they provide are compiled at installation time. So they
 are directly accessible with the command ``Require`` (see
-Section :ref:`TODO-6.5.1-Require`).
+Section :ref:`compiled-files`).
 
 The different modules of the |Coq| standard library are documented
 online at http://coq.inria.fr/stdlib.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 687775980..ce10c651a 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -183,7 +183,7 @@ other arguments are the parameters of the inductive type.
 .. note:: Induction schemes are automatically generated for inductive records.
    Automatic generation of induction schemes for non-recursive records
    defined with the ``Record`` keyword can be activated with the
-   ``Nonrecursive Elimination Schemes`` option (see :ref:`TODO-13.1.1-nonrecursive-elimination-schemes`).
+   ``Nonrecursive Elimination Schemes`` option (see :ref:`proofschemes-induction-principles`).
 
 .. note:: ``Structure`` is a synonym of the keyword ``Record``.
 
@@ -195,7 +195,7 @@ other arguments are the parameters of the inductive type.
 
   #. The name `ident` already exists in the environment (see Section :ref:`TODO-1.3.1-axioms`).
   #. The body of `ident` uses an incorrect elimination for
-     `ident` (see Sections :ref:`TODO-1.3.4-fixpoint` and :ref:`TODO-4.5.3-case-expr`).
+     `ident` (see Sections :ref:`TODO-1.3.4-fixpoint` and :ref:`Destructors`).
   #. The type of the projections `ident` depends on previous
      projections which themselves could not be defined.
 
@@ -214,7 +214,7 @@ During the definition of the one-constructor inductive definition, all
 the errors of inductive definitions, as described in Section
 :ref:`TODO-1.3.3-inductive-definitions`, may also occur.
 
-**See also** Coercions and records in Section :ref:`TODO-18.9-coercions-and-records` of the chapter devoted to coercions.
+**See also** Coercions and records in Section :ref:`coercions-classes-as-records` of the chapter devoted to coercions.
 
 .. _primitive_projections:
 
@@ -626,7 +626,7 @@ The following experimental command is available when the ``FunInd`` library has
 This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper
 for several ways of defining a function *and other useful related
 objects*, namely: an induction principle that reflects the recursive
-structure of the function (see Section :ref:`TODO-8.5.5-functional-induction`) and its fixpoint equality.
+structure of the function (see :tacn:`function induction`) and its fixpoint equality.
 The meaning of this declaration is to define a function ident,
 similarly to ``Fixpoint`. Like in ``Fixpoint``, the decreasing argument must
 be given (unless the function is not recursive), but it might not
@@ -639,8 +639,8 @@ The ``Function`` construction also enjoys the ``with`` extension to define
 mutually recursive definitions. However, this feature does not work
 for non structurally recursive functions.
 
-See the documentation of functional induction (:ref:`TODO-8.5.5-functional-induction`)
-and ``Functional Scheme`` (:ref:`TODO-13.2-functional-scheme`) for how to use
+See the documentation of functional induction (:tacn:`function induction`)
+and ``Functional Scheme`` (:ref:`functional-scheme`) for how to use
 the induction principle to easily reason about the function.
 
 Remark: To obtain the right principle, it is better to put rigid
@@ -711,7 +711,7 @@ terminating functions.
 
      `functional inversion` will not be available for the function.
 
-See also: :ref:`TODO-13.2-generating-ind-principles` and ref:`TODO-8.5.5-functional-induction`
+See also: :ref:`functional-scheme` and :tacn:`function induction`
 
 Depending on the ``{…}`` annotation, different definition mechanisms are
 used by ``Function``. A more precise description is given below.
@@ -771,6 +771,7 @@ used by ``Function``. A more precise description is given below.
    hand. Remark: Proof obligations are presented as several subgoals
    belonging to a Lemma `ident`\ :math:`_{\sf tcc}`.
 
+.. _section-mechanism:
 
 Section mechanism
 -----------------
@@ -847,7 +848,7 @@ together, as well as a means of massive abstraction.
 
 In the syntax of module application, the ! prefix indicates that any
 `Inline` directive in the type of the functor arguments will be ignored
-(see :ref:`named_module_type` below).
+(see the ``Module Type`` command below).
 
 
 .. cmd:: Module @ident.
@@ -933,8 +934,6 @@ Reserved commands inside an interactive module
 
        is equivalent to an interactive module where each `module_expression` is included.
 
-.. _named_module_type:
-
 .. cmd:: Module Type @ident.
 
 This command is used to start an interactive module type `ident`.
@@ -1195,7 +1194,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
        Check T.
 
 Some features defined in modules are activated only when a module is
-imported. This is for instance the case of notations (see :ref:`TODO-12.1-Notations`).
+imported. This is for instance the case of notations (see :ref:`Notations`).
 
 Declarations made with the Local flag are never imported by theImport
 command. Such declarations are only accessible through their fully
@@ -1248,6 +1247,8 @@ qualified name.
 Libraries and qualified names
 ---------------------------------
 
+.. _names-of-libraries:
+
 Names of libraries
 ~~~~~~~~~~~~~~~~~~
 
@@ -1260,10 +1261,11 @@ identifiers qualid, i.e. as list of identifiers separated by dots (see
 the name of a library is called a *library root*. All library files of
 the standard library of |Coq| have the reserved root |Coq| but library
 file names based on other roots can be obtained by using |Coq| commands
-(coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`TODO-14.3.3-command-line-options`).
+(coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`).
 Also, when an interactive |Coq| session starts, a library of root ``Top`` is
-started, unless option ``-top`` or ``-notop`` is set (see :ref:`TODO-14.3.3-command-line-options`).
+started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`).
 
+.. _qualified-names:
 
 Qualified names
 ~~~~~~~~~~~~~~~
@@ -1298,7 +1300,7 @@ names also applies to library file names.
 
 |Coq| maintains a table called the name table which maps partially qualified
 names of constructions to absolute names. This table is updated by the
-commands ``Require`` (see :ref:`TODO-6.5.1-Require`), Import and Export (see :ref:`import_qualid`) and
+commands ``Require`` (see :ref:`compiled-files`), ``Import`` and ``Export`` (see :ref:`here <import_qualid>`) and
 also each time a new declaration is added to the context. An absolute
 name is called visible from a given short or partially qualified name
 when this latter name is enough to denote it. This means that the
@@ -1329,13 +1331,13 @@ accessible, absolute names can never be hidden.
 See also: Command Locate in :ref:`TODO-6.3.10-locate-qualid` and Locate Library in
 :ref:`TODO-6.6.11-locate-library`.
 
+.. _libraries-and-filesystem:
 
 Libraries and filesystem
 ~~~~~~~~~~~~~~~~~~~~~~~~
 
-Please note that the questions described here have been subject to
-redesign in |Coq| v8.5. Former versions of |Coq| use the same terminology
-to describe slightly different things.
+.. note:: The questions described here have been subject to redesign in |Coq| 8.5.
+   Former versions of |Coq| use the same terminology to describe slightly different things.
 
 Compiled files (``.vo`` and ``.vio``) store sub-libraries. In order to refer
 to them inside |Coq|, a translation from file-system names to |Coq| names
@@ -1371,7 +1373,7 @@ translation and with an empty logical prefix.
 The command line option ``-R`` is a variant of ``-Q`` which has the strictly
 same behavior regarding loadpaths, but which also makes the
 corresponding ``.vo`` files available through their short names in a way
-not unlike the ``Import`` command (see :ref:`import_qualid`). For instance, ``-R`` `path` ``Lib``
+not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R`` `path` ``Lib``
 associates to the ``filepath/fOO/Bar/File.vo`` the logical name
 ``Lib.fOO.Bar.File``, but allows this file to be accessed through the
 short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with
@@ -1379,7 +1381,7 @@ identical base name are present in different subdirectories of a
 recursive loadpath, which of these files is found first may be system-
 dependent and explicit qualification is recommended. The ``From`` argument
 of the ``Require`` command can be used to bypass the implicit shortening
-by providing an absolute root to the required file (see :ref:`TODO-6.5.1-require-qualid`).
+by providing an absolute root to the required file (see :ref:`compiled-files`).
 
 There also exists another independent loadpath mechanism attached to
 OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object
@@ -1387,11 +1389,12 @@ files as described above. The OCaml loadpath is managed using
 the option ``-I`` `path` (in the OCaml world, there is neither a
 notion of logical name prefix nor a way to access files in
 subdirectories of path). See the command ``Declare`` ``ML`` ``Module`` in
-:ref:`TODO-6.5-compiled-files` to understand the need of the OCaml loadpath.
+:ref:`compiled-files` to understand the need of the OCaml loadpath.
 
-See :ref:`TODO-14.3.3-command-line-options` for a more general view over the |Coq| command
+See :ref:`command-line-options` for a more general view over the |Coq| command
 line options.
 
+.. _ImplicitArguments:
 
 Implicit arguments
 ------------------
@@ -2098,6 +2101,7 @@ implicitly, as maximally-inserted arguments. In these binders, the
 binding name for the bound object is optional, whereas the type is
 mandatory, dually to regular binders.
 
+.. _Coercions:
 
 Coercions
 ---------
@@ -2136,19 +2140,21 @@ Otherwise said, ``Set Printing All`` includes the effects of the commands
 ``Unset Printing Projections``, and ``Unset Printing Notations``. To reactivate
 the high-level printing features, use the command ``Unset Printing All``.
 
+.. _printing-universes:
+
 Printing universes
 ------------------
 
 .. opt:: Printing Universes.
 
 Turn this option on to activate the display of the actual level of each occurrence of ``Type``.
-See :ref:`TODO-4.1.1-sorts` for details. This wizard option, in combination
+See :ref:`Sorts` for details. This wizard option, in combination
 with ``Set Printing All`` (see :ref:`printing_constructions_full`) can help to diagnose failures
 to unify terms apparently identical but internally different in the
 Calculus of Inductive Constructions.
 
 The constraints on the internal level of the occurrences of Type
-(see :ref:`TODO-4.1.1-sorts`) can be printed using the command
+(see :ref:`Sorts`) can be printed using the command
 
 .. cmd:: Print {? Sorted} Universes.
 
@@ -2164,6 +2170,7 @@ If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
 language, and can be processed by Graphviz tools. The format is
 unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
 
+.. _existential-variables:
 
 Existential variables
 ---------------------
@@ -2173,9 +2180,9 @@ subterms to eventually be replaced by actual subterms.
 
 Existential variables are generated in place of unsolvable implicit
 arguments or “_” placeholders when using commands such as ``Check`` (see
-Section :ref:`TODO-6.3.1-check`) or when using tactics such as ``refine`` (see Section
-:ref:`TODO-8.2.3-refine`), as well as in place of unsolvable instances when using
-tactics such that ``eapply`` (see Section :ref:`TODO-8.2.4-apply`). An existential
+Section :ref:`requests-to-the-environment`) or when using tactics such as
+:tacn:`refine`, as well as in place of unsolvable instances when using
+tactics such that :tacn:`eapply`. An existential
 variable is defined in a context, which is the context of variables of
 the placeholder which generated the existential variable, and a type,
 which is the expected type of the placeholder.
@@ -2256,5 +2263,5 @@ using highly automated tactics without resorting to writing the proof-term
 by means of the interactive proof engine.
 
 This mechanism is comparable to the ``Declare Implicit Tactic`` command
-defined at :ref:`TODO-8.9.7-implicit-automation`, except that the used
+defined at :ref:`tactics-implicit-automation`, except that the used
 tactic is local to each hole instead of being declared globally.
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 2a146c57a..6458ceeaa 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -13,7 +13,7 @@ language of commands, called *The Vernacular* is described in Section
 :ref:`vernacular`.
 
 In Coq, logical objects are typed to ensure their logical correctness.  The
-rules implemented by the typing algorithm are described in Chapter :ref:`cic`.
+rules implemented by the typing algorithm are described in Chapter :ref:`calculusofinductiveconstructions`.
 
 
 About the grammars in the manual
@@ -110,6 +110,8 @@ Special tokens
   longest possible one (among all tokens defined at this moment), and so
   on.
 
+.. _term:
+
 Terms
 =====
 
@@ -118,9 +120,9 @@ Syntax of terms
 
 The following grammars describe the basic syntax of the terms of the
 *Calculus of Inductive Constructions* (also called Cic). The formal
-presentation of Cic is given in Chapter :ref:`cic`. Extensions of this syntax
-are given in Chapter :ref:`gallinaextensions`. How to customize the syntax
-is described in Chapter :ref:`syntaxextensions`.
+presentation of Cic is given in Chapter :ref:`calculusofinductiveconstructions`. Extensions of this syntax
+are given in Chapter :ref:`extensionsofgallina`. How to customize the syntax
+is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
 
 .. productionlist:: coq
    term             : forall `binders` , `term`
@@ -201,9 +203,9 @@ Numerals
 
 Numerals have no definite semantics in the calculus. They are mere
 notations that can be bound to objects through the notation mechanism
-(see Chapter :ref:`syntaxextensions` for details).
+(see Chapter :ref:`syntaxextensionsandinterpretationscopes` for details).
 Initially, numerals are bound to Peano’s representation of natural
-numbers (see :ref:`libnats`).
+numbers (see :ref:`datatypes`).
 
 .. note::
 
@@ -484,6 +486,8 @@ The association of a single fixpoint and a local definition have a special
 syntax: “let fix f … := … in …” stands for “let f := fix f … := … in …”. The
 same applies for co-fixpoints.
 
+.. _vernacular:
+
 The Vernacular
 ==============
 
@@ -605,6 +609,8 @@ logical postulates (i.e. when the assertion *term* is of sort ``Prop``),
 and to use the keywords ``Parameter`` and ``Variable`` in other cases
 (corresponding to the declaration of an abstract mathematical entity).
 
+.. _gallina_def:
+
 Definitions
 -----------
 
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 1ff808894..9f485f496 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -16,6 +16,8 @@ The options are (basically) the same for the first two commands, and
 roughly described below. You can also look at the ``man`` pages of
 ``coqtop`` and ``coqc`` for more details.
 
+.. _interactive-use:
+
 Interactive use (coqtop)
 ------------------------
 
@@ -39,10 +41,12 @@ Batch compilation (coqc)
 
 The ``coqc`` command takes a name *file* as argument. Then it looks for a
 vernacular file named *file*.v, and tries to compile it into a
-*file*.vo file (See :ref:`TODO-6.5`). Warning: The name *file* should be a
-regular |Coq| identifier, as defined in Section :ref:'TODO-1.1'. It should contain
-only letters, digits or underscores (_). For instance, ``/bar/foo/toto.v`` is valid, but
-``/bar/foo/to-to.v`` is invalid.
+*file*.vo file (See :ref:`compiled-files`).
+
+.. caution:: The name *file* should be a
+   regular |Coq| identifier, as defined in Section :ref:'TODO-1.1'. It should contain
+   only letters, digits or underscores (_). For instance, ``/bar/foo/toto.v`` is valid, but
+   ``/bar/foo/to-to.v`` is invalid.
 
 
 Customization at launch time
@@ -63,6 +67,7 @@ This file may contain, for instance, ``Add LoadPath`` commands to add
 directories to the load path of |Coq|. It is possible to skip the
 loading of the resource file with the option ``-q``.
 
+.. _customization-by-environment-variables:
 
 By environment variables
 ~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -70,7 +75,7 @@ By environment variables
 Load path can be specified to the |Coq| system by setting up ``$COQPATH``
 environment variable. It is a list of directories separated by
 ``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and
-``$XDG_DATA_DIRS`` (see Section :ref:`TODO-2.6.3`).
+``$XDG_DATA_DIRS`` (see Section :ref:`libraries-and-filesystem`).
 
 Some |Coq| commands call other |Coq| commands. In this case, they look for
 the commands in directory specified by ``$COQBIN``. If this variable is
@@ -84,6 +89,8 @@ list of assignments of the form ``name=``:n:``{*; attr}`` where
 ANSI escape code. The list of highlight tags can be retrieved with the
 ``-list-tags`` command-line option of ``coqtop``.
 
+.. _command-line-options:
+
 By command line options
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -91,13 +98,13 @@ The following command-line options are recognized by the commands ``coqc``
 and ``coqtop``, unless stated otherwise:
 
 :-I *directory*, -include *directory*: Add physical path *directory*
-  to the OCaml loadpath. See also: :ref:`TODO-2.6.1` and the
-  command Declare ML Module Section :ref:`TODO-6.5`.
+  to the OCaml loadpath. See also: :ref:`names-of-libraries` and the
+  command Declare ML Module Section :ref:`compiled-files`.
 :-Q *directory* dirpath: Add physical path *directory* to the list of
   directories where |Coq| looks for a file and bind it to the the logical
   directory *dirpath*. The subdirectory structure of *directory* is
   recursively available from |Coq| using absolute names (extending the
-  dirpath prefix) (see Section :ref:`TODO-2.6.2`).Note that only those
+  dirpath prefix) (see Section :ref:`qualified-names`).Note that only those
   subdirectories and files which obey the lexical conventions of what is
   an ident (see Section :ref:`TODO-1.1`) are taken into account. Conversely, the
   underlying file systems or operating systems may be more restrictive
@@ -105,11 +112,11 @@ and ``coqtop``, unless stated otherwise:
   layout (within the limit of 255 bytes per file name), the default on
   NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to
   disallow two files differing only in the case in the same directory.
-  See also: Section :ref:`TODO-2.6.1`.
+  See also: Section :ref:`names-of-libraries`.
 :-R *directory* dirpath: Do as -Q *directory* dirpath but make the
   subdirectory structure of *directory* recursively visible so that the
   recursive contents of physical *directory* is available from |Coq| using
-  short or partially qualified names. See also: Section :ref:`TODO-2.6.1`.
+  short or partially qualified names. See also: Section :ref:`names-of-libraries`.
 :-top dirpath: Set the toplevel module name to dirpath instead of Top.
   Not valid for `coqc` as the toplevel module name is inferred from the
   name of the output file.
@@ -145,7 +152,7 @@ and ``coqtop``, unless stated otherwise:
   -compile-verbose.
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
   option expects all, none or a comma-separated list of warning names or
-  categories (see Section :ref:`TODO-6.9.3`).
+  categories (see Section :ref:`controlling-display`).
 :-color (on|off|auto): Enable or not the coloring of output of `coqtop`.
   Default is auto, meaning that `coqtop` dynamically decides, depending on
   whether the output channel supports ANSI escape sequences.
@@ -170,7 +177,7 @@ and ``coqtop``, unless stated otherwise:
 :-compat *version*: Attempt to maintain some backward-compatibility
   with a previous version.
 :-dump-glob *file*: Dump references for global names in file *file*
-  (to be used by coqdoc, see :ref:`TODO-15.4`). By default, if *file.v* is being
+  (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being
   compiled, *file.glob* is used.
 :-no-glob: Disable the dumping of references for global names.
 :-image *file*: Set the binary image to be used by `coqc` to be *file*
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index a3b942628..3d144b1d6 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -75,7 +75,7 @@ There are two additional buttons for navigation within the running buffer. The
 "down" button with a line goes directly to the end; the "up" button with a line
 goes back to the beginning. The handling of errors when using the go-to-the-end
 button depends on whether |Coq| is running in asynchronous mode or not (see
-Chapter :ref:`Asyncprocessing`). If it is not running in that mode, execution
+Chapter :ref:`asynchronousandparallelproofprocessing`). If it is not running in that mode, execution
 stops as soon as an error is found. Otherwise, execution continues, and the
 error is marked with an underline in the error foreground color, with a
 background in the error background color (pink by default). The same
@@ -90,10 +90,10 @@ There are other buttons on the |CoqIDE| toolbar: a button to save the running
 buffer; a button to close the current buffer (an "X"); buttons to switch among
 buffers (left and right arrows); an "information" button; and a "gears" button.
 
-The "information" button is described in Section :ref:`sec:trytactics`.
+The "information" button is described in Section :ref:`try-tactics-automatically`.
 
 The "gears" button submits proof terms to the |Coq| kernel for type-checking.
-When |Coq| uses asynchronous processing (see Chapter :ref:`Asyncprocessing`),
+When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`),
 proofs may have been completed without kernel-checking of generated proof terms.
 The presence of unchecked proof terms is indicated by ``Qed`` statements that
 have a subdued *being-processed* color (light blue by default), rather than the
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 620c002ff..48d58c473 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -33,6 +33,7 @@ For example, to statically link |L_tac|, you can just do:
    % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
                  -package coq.toplevel -package coq.ltac \
                  toplevel/coqtop\_bin.ml -o my\_toplevel.native
+
 and similarly for other plugins.
 
 
@@ -43,7 +44,7 @@ The majority of |Coq| projects are very similar: a collection of ``.v``
 files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of
 metadata needed in order to build the project are the command line
 options to ``coqc`` (e.g. ``-R``, ``-I``, see also: Section
-:ref:`bycommandline`). Collecting the list of files and options is the job
+:ref:`command-line-options`). Collecting the list of files and options is the job
 of the ``_CoqProject`` file.
 
 A simple example of a ``_CoqProject`` file follows:
@@ -59,7 +60,7 @@ A simple example of a ``_CoqProject`` file follows:
     src/qux_plugin.mlpack
 
 
-Currently, both |CoqIDE| and |ProofGeneral| (version ≥ ``4.3pre``)
+Currently, both |CoqIDE| and Proof-General (version ≥ ``4.3pre``)
 understand ``_CoqProject`` files and invoke |Coq| with the desired options.
 
 The ``coq_makefile`` utility can be used to set up a build infrastructure
@@ -77,7 +78,7 @@ CoqMakefile
   is a generic makefile for ``GNU Make`` that provides
   targets to build the project (both ``.v`` and ``.ml*`` files), to install it
   system-wide in the ``coq-contrib`` directory (i.e. where |Coq| is installed)
-  as well as to invoke |coqdoc| to generate |HTML| documentation.
+  as well as to invoke coqdoc to generate HTML documentation.
 
 CoqMakefile.conf
   contains make variables assignments that reflect
@@ -89,7 +90,7 @@ An optional file ``CoqMakefile.local`` can be provided by the user in order to
 extend ``CoqMakefile``. In particular one can declare custom actions to be
 performed before or after the build process. Similarly one can customize the
 install target or even provide new targets. Extension points are documented in
-paragraph :ref:`coqmakefile:local`.
+paragraph :ref:`coqmakefilelocal`.
 
 The extensions of the files listed in ``_CoqProject`` is used in order to
 decide how to build them. In particular:
@@ -120,25 +121,33 @@ CoqMakefile.local
 The optional file ``CoqMakefile.local`` is included by the generated
 file ``CoqMakefile``. It can contain two kinds of directives.
 
-Variable assignment
-  The variable must belong to the variables listed in the ``Parameters`` section of the generated makefile.
-  Here we describe only few of them.
-    :CAMLPKGS:
-      can be used to specify third party findlib packages, and is
-      passed to the OCaml compiler on building or linking of modules. Eg:
-      ``-package yojson``.
-    :CAMLFLAGS:
-      can be used to specify additional flags to the |OCaml|
-      compiler, like ``-bin-annot`` or ``-w``....
-    :COQC, COQDEP, COQDOC:
-      can be set in order to use alternative binaries
-      (e.g. wrappers)
-    :COQ_SRC_SUBDIRS: can be extended by including other paths in which ``*.cm*`` files are searched. For example ``COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq`` lets you build a plugin containing OCaml code that depends on the OCaml code of ``Unicoq``.
-
-Rule extension
-  The following makefile rules can be extended.
-
-  .. example ::
+**Variable assignment**
+
+The variable must belong to the variables listed in the ``Parameters``
+section of the generated makefile.
+Here we describe only few of them.
+
+:CAMLPKGS:
+   can be used to specify third party findlib packages, and is
+   passed to the OCaml compiler on building or linking of modules. Eg:
+   ``-package yojson``.
+:CAMLFLAGS:
+   can be used to specify additional flags to the |OCaml|
+   compiler, like ``-bin-annot`` or ``-w``....
+:COQC, COQDEP, COQDOC:
+   can be set in order to use alternative binaries
+   (e.g. wrappers)
+:COQ_SRC_SUBDIRS:
+   can be extended by including other paths in which ``*.cm*`` files
+   are searched. For example ``COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq``
+   lets you build a plugin containing OCaml code that depends on the
+   OCaml code of ``Unicoq``.
+
+**Rule extension**
+
+The following makefile rules can be extended.
+
+.. example::
 
     ::
 
@@ -147,39 +156,38 @@ Rule extension
         install-extra::
                 cp ThisExtraFile /there/it/goes
 
-  ``pre-all::``
-    run before the all target. One can use this to configure
-   the project, or initialize sub modules or check dependencies are met.
+``pre-all::``
+  run before the ``all`` target. One can use this to configure
+  the project, or initialize sub modules or check dependencies are met.
 
-  ``post-all::``
-    run after the all target. One can use this to run a test
-    suite, or compile extracted code.
+``post-all::``
+  run after the ``all`` target. One can use this to run a test
+  suite, or compile extracted code.
 
+``install-extra::``
+  run after ``install``. One can use this to install extra files.
 
-  ``install-extra::``
-    run after install. One can use this to install extra files.
+``install-doc::``
+  One can use this to install extra doc.
 
-  ``install-doc::``
-    One can use this to install extra doc.
+``uninstall::``
+  \
 
-  ``uninstall::``
-    \
+``uninstall-doc::``
+  \
 
-  ``uninstall-doc::``
-    \
+``clean::``
+  \
 
-  ``clean::``
-    \
+``cleanall::``
+  \
 
-  ``cleanall::``
-    \
+``archclean::``
+  \
 
-  ``archclean::``
-    \
-
-  ``merlin-hook::``
-    One can append lines to the generated .merlin file extending this
-    target.
+``merlin-hook::``
+  One can append lines to the generated ``.merlin`` file extending this
+  target.
 
 Timing targets and performance testing
 ++++++++++++++++++++++++++++++++++++++
@@ -311,8 +319,8 @@ line timing data:
 
 + ``print-pretty-single-time-diff``
     ::
-
        print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing
+
     this target will make a sorted table of the per-line timing differences
     between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and
     save it to the file specified by the ``TIME_OF_PRETTY_BUILD_FILE`` variable,
@@ -451,14 +459,16 @@ automatically compute the dependencies among the files part of the
 project.
 
 
+.. _coqdoc:
+
 Documenting |Coq| files with coqdoc
 -----------------------------------
 
-|coqdoc| is a documentation tool for the proof assistant |Coq|, similar to
-``javadoc`` or ``ocamldoc``. The task of |coqdoc| is
+coqdoc is a documentation tool for the proof assistant |Coq|, similar to
+``javadoc`` or ``ocamldoc``. The task of coqdoc is
 
 
-#. to produce a nice |Latex| and/or |HTML| document from the |Coq|
+#. to produce a nice |Latex| and/or HTML document from the |Coq|
    sources, readable for a human and not only for the proof assistant;
 #. to help the user navigating in his own (or third-party) sources.
 
@@ -468,18 +478,18 @@ Principles
 ~~~~~~~~~~
 
 Documentation is inserted into |Coq| files as *special comments*. Thus
-your files will compile as usual, whether you use |coqdoc| or not. |coqdoc|
+your files will compile as usual, whether you use coqdoc or not. coqdoc
 presupposes that the given |Coq| files are well-formed (at least
 lexically). Documentation starts with ``(**``, followed by a space, and
 ends with the pending ``*)``. The documentation format is inspired by Todd
 A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with
-some syntax-light controls, described below. |coqdoc| is robust: it
+some syntax-light controls, described below. coqdoc is robust: it
 shouldn’t fail, whatever the input is. But remember: “garbage in,
 garbage out”.
 
 
 |Coq| material inside documentation.
-++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++
 
 |Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets
 may be nested, the inner ones being understood as being part of the
@@ -494,7 +504,7 @@ followed by a newline and the latter must follow a newline.
 Pretty-printing.
 ++++++++++++++++
 
-|coqdoc| uses different faces for identifiers and keywords. The pretty-
+coqdoc uses different faces for identifiers and keywords. The pretty-
 printing of |Coq| tokens (identifiers or symbols) can be controlled
 using one of the following commands:
 
@@ -512,8 +522,8 @@ or
     (** printing  *token* $...LATEX math...$ #...html...# *)
 
 
-It gives the |Latex| and |HTML| texts to be produced for the given |Coq|
-token. One of the |Latex| or |HTML| text may be omitted, causing the
+It gives the |Latex| and HTML texts to be produced for the given |Coq|
+token. One of the |Latex| or HTML text may be omitted, causing the
 default pretty-printing to be used for this token.
 
 The printing for one token can be removed with
@@ -614,18 +624,18 @@ emphasis. Usually, these are spaces or punctuation.
 
 
 
-Escaping to |Latex| and |HTML|.
+Escaping to |Latex| and HTML.
 +++++++++++++++++++++++++++++++
 
-Pure |Latex| or |HTML| material can be inserted using the following
+Pure |Latex| or HTML material can be inserted using the following
 escape sequences:
 
 
 + ``$...LATEX stuff...$`` inserts some |Latex| material in math mode.
-  Simply discarded in |HTML| output.
+  Simply discarded in HTML output.
 + ``%...LATEX stuff...%`` inserts some |Latex| material. Simply
-  discarded in |HTML| output.
-+ ``#...HTML stuff...#`` inserts some |HTML| material. Simply discarded in
+  discarded in HTML output.
++ ``#...HTML stuff...#`` inserts some HTML material. Simply discarded in
   |Latex| output.
 
 .. note::
@@ -654,7 +664,7 @@ at the beginning of a line.
 Hyperlinks
 ++++++++++
 
-Hyperlinks can be inserted into the |HTML| output, so that any
+Hyperlinks can be inserted into the HTML output, so that any
 identifier is linked to the place of its definition.
 
 ``coqc file.v`` automatically dumps localization information in
@@ -662,7 +672,7 @@ identifier is linked to the place of its definition.
 file``. Take care of erasing this global file, if any, when starting
 the whole compilation process.
 
-Then invoke |coqdoc| or ``coqdoc --glob-from file`` to tell |coqdoc| to look
+Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look
 for name resolutions into the file ``file`` (it will look in ``file.glob``
 by default).
 
@@ -703,17 +713,17 @@ be used around a whole proof.
 Usage
 ~~~~~
 
-|coqdoc| is invoked on a shell command line as follows:
+coqdoc is invoked on a shell command line as follows:
 ``coqdoc <options and files>``.
 Any command line argument which is not an option is considered to be a
 file (even if it starts with a ``-``). |Coq| files are identified by the
 suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``.
 
 
-:|HTML| output: This is the default output. One |HTML| file is created for
+:HTML output: This is the default output. One HTML file is created for
   each |Coq| file given on the command line, together with a file
-  ``index.html`` (unless ``option-no-index is passed``). The |HTML| pages use a
-  style sheet named ``style.css``. Such a file is distributed with |coqdoc|.
+  ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a
+  style sheet named ``style.css``. Such a file is distributed with coqdoc.
 :|Latex| output: A single |Latex| file is created, on standard
   output. It can be redirected to a file with option ``-o``. The order of
   files on the command line is kept in the final document. |Latex|
@@ -732,7 +742,7 @@ Command line options
 **Overall options**
 
 
-  :--|HTML|: Select a |HTML| output.
+  :--HTML: Select a HTML output.
   :--|Latex|: Select a |Latex| output.
   :--dvi: Select a DVI output.
   :--ps: Select a PostScript output.
@@ -760,7 +770,7 @@ Command line options
 
 **Index options**
 
-  Default behavior is to build an index, for the |HTML| output only,
+  Default behavior is to build an index, for the HTML output only,
   into ``index.html``.
 
   :--no-index: Do not output the index.
@@ -775,7 +785,7 @@ Command line options
 
   :-toc, --table-of-contents: Insert a table of contents. For a |Latex|
     output, it inserts a ``\tableofcontents`` at the beginning of the
-    document. For a |HTML| output, it builds a table of contents into
+    document. For a HTML output, it builds a table of contents into
     ``toc.html``.
   :--toc-depth int: Only include headers up to depth ``int`` in the table of
     contents.
@@ -803,20 +813,18 @@ Command line options
 **Title options**
 
   :-s , --short: Do not insert titles for the files. The default
-    behavior is to insert a title like “Library Foo” for each file.
+     behavior is to insert a title like “Library Foo” for each file.
   :--lib-name string: Print “string Foo” instead of “Library Foo” in
-    titles. For example “Chapter” and “Module” are reasonable choices.
+     titles. For example “Chapter” and “Module” are reasonable choices.
   :--no-lib-name: Print just “Foo” instead of “Library Foo” in titles.
   :--lib-subtitles: Look for library subtitles. When enabled, the
-  beginning of each file is checked for a comment of the form:
-
-  ::
-
+     beginning of each file is checked for a comment of the form:
 
-      (** * ModuleName : text *)
+     ::
+        (** * ModuleName : text *)
 
-  where ``ModuleName`` must be the name of the file. If it is present, the
-    text is used as a subtitle for the module in appropriate places.
+     where ``ModuleName`` must be the name of the file. If it is present, the
+     text is used as a subtitle for the module in appropriate places.
   :-t string, --title string: Set the document title.
 
 
@@ -854,11 +862,11 @@ Command line options
   :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to
     --inputenc latin1 --charset iso-8859-1.
   :-utf8, --utf8: Set --inputenc utf8x for |Latex| output and--charset
-    utf-8 for |HTML| output. Also use Unicode replacements for a couple of
+    utf-8 for HTML output. Also use Unicode replacements for a couple of
     standard plain ASCII notations such as → for ``->`` and ∀ for ``forall``. |Latex|
     UTF-8 support can be found
     at `<http://www.ctan.org/pkg/unicode>`_. For the interpretation of Unicode
-    characters by |Latex|, extra packages which |coqdoc| does not provide
+    characters by |Latex|, extra packages which coqdoc does not provide
     by default might be required, such as textgreek for some Greek letters
     or ``stmaryrd`` for some mathematical symbols. If a Unicode character is
     missing an interpretation in the utf8x input encoding, add
@@ -866,13 +874,13 @@ Command line options
     and declarations can be added with option ``-p``.
   :--inputenc string: Give a |Latex| input encoding, as an option to |Latex|
     package ``inputenc``.
-  :--charset string: Specify the |HTML| character set, to be inserted in
-    the |HTML| header.
+  :--charset string: Specify the HTML character set, to be inserted in
+    the HTML header.
 
 
 
 The coqdoc |Latex| style file
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 In case you choose to produce a document without the default |Latex|
 preamble (by using option ``--no-preamble``), then you must insert into
@@ -929,16 +937,16 @@ There are options to produce the |Coq| parts in smaller font, italic,
 between horizontal rules, etc. See the man page of ``coq-tex`` for more
 details.
 
-|Coq| and |GNU| |Emacs|
+|Coq| and GNU Emacs
 -----------------------
 
 
-The |Coq| |Emacs| mode
+The |Coq| Emacs mode
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
-|Coq| comes with a Major mode for |GNU| |Emacs|, ``gallina.el``. This mode
+|Coq| comes with a Major mode for GNU Emacs, ``gallina.el``. This mode
 provides syntax highlighting and also a rudimentary indentation
-facility in the style of the ``Caml`` |GNU| |Emacs| mode.
+facility in the style of the ``Caml`` GNU Emacs mode.
 
 Add the following lines to your ``.emacs`` file:
 
@@ -956,26 +964,26 @@ facility:
 
 + pressing ``Tab`` at the beginning of a line indents the line like the
   line above;
-+ extra ``Tab``s increase the indentation level (by 2 spaces by default);
++ extra tabulations increase the indentation level (by 2 spaces by default);
 + ``M-Tab`` decreases the indentation level.
 
 
-An inferior mode to run |Coq| under |Emacs|, by Marco Maggesi, is also
+An inferior mode to run |Coq| under Emacs, by Marco Maggesi, is also
 included in the distribution, in file ``inferior-coq.el``. Instructions to
 use it are contained in this file.
 
 
-Proof General
+Proof-General
 ~~~~~~~~~~~~~
 
-|ProofGeneral| is a generic interface for proof assistants based on
-|Emacs|. The main idea is that the |Coq| commands you are editing are sent
-to a |Coq| toplevel running behind |Emacs| and the answers of the system
-automatically inserted into other |Emacs| buffers. Thus you don’t need
+Proof-General is a generic interface for proof assistants based on
+Emacs. The main idea is that the |Coq| commands you are editing are sent
+to a |Coq| toplevel running behind Emacs and the answers of the system
+automatically inserted into other Emacs buffers. Thus you don’t need
 to copy-paste the |Coq| material from your files to the |Coq| toplevel or
 conversely from the |Coq| toplevel to some files.
 
-|ProofGeneral| is developed and distributed independently of the system
+Proof-General is developed and distributed independently of the system
 |Coq|. It is freely available at `<https://proofgeneral.github.io/>`_.
 
 
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
diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst
index 0fee3754b..28a04f90c 100644
--- a/doc/sphinx/replaces.rst
+++ b/doc/sphinx/replaces.rst
@@ -35,6 +35,7 @@
 .. |ident_n,1| replace:: `ident`\ :math:`_{n,1}`
 .. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}`
 .. |ident_n| replace:: `ident`\ :math:`_{n}`
+.. |Latex| replace:: :smallcaps:`LaTeX`
 .. |L_tac| replace:: `L`:sub:`tac`
 .. |Ltac| replace:: `L`:sub:`tac`
 .. |ML| replace:: :smallcaps:`ML`
@@ -55,7 +56,7 @@
 .. |module_type_n| replace:: `module_type`\ :math:`_{n}`
 .. |N| replace:: ``N``
 .. |nat| replace:: ``nat``
-.. |Ocaml| replace:: :smallcaps:`OCaml`
+.. |OCaml| replace:: :smallcaps:`OCaml`
 .. |p_1| replace:: `p`\ :math:`_{1}`
 .. |p_i| replace:: `p`\ :math:`_{i}`
 .. |p_n| replace:: `p`\ :math:`_{n}`
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 583b73e53..1f1167c59 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -3,6 +3,8 @@
 Proof schemes
 ===============
 
+.. _proofschemes-induction-principles:
+
 Generation of induction principles with ``Scheme``
 --------------------------------------------------------
 
@@ -163,6 +165,8 @@ concluded by the conjunction of their conclusions.
 
     Check tree_forest_mutind.
 
+.. _functional-scheme:
+
 Generation of induction principles with ``Functional`` ``Scheme``
 -----------------------------------------------------------------
 
@@ -229,7 +233,7 @@ definition written by the user.
     simpl; auto with arith.
     Qed.
 
-  We can use directly the functional induction (:ref:`TODO-8.5.5`) tactic instead
+  We can use directly the functional induction (:tacn:`function induction`) tactic instead
   of the pattern/apply trick:
 
   .. coqtop:: all
@@ -305,6 +309,8 @@ definition written by the user.
   .. coqtop:: all
 
     Check tree_size_ind2.
+
+.. _derive-inversion:
      
 Generation of inversion principles with ``Derive`` ``Inversion``
 -----------------------------------------------------------------
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 531295b63..0da9f2300 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -381,6 +381,8 @@ Displaying informations about notations
    :opt:`Printing All`
       To disable other elements in addition to notations.
 
+.. _locating-notations:
+
 Locating notations
 ~~~~~~~~~~~~~~~~~~
 
@@ -491,7 +493,7 @@ the following:
 
 This is so because the grammar also contains rules starting with :g:`{}` and
 followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the
-constant :g:`sumbool` (see Section :ref:`sumbool`).
+constant :g:`sumbool` (see Section :ref:`specification`).
 
 Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning
 that ``x`` is parsed as a term at level 99 (as done in the notation for
@@ -829,6 +831,8 @@ lonely notations. These scopes, in opening order, are ``core_scope``,
    These variants survive sections. They behave as if Global were absent when
    not inside a section.
 
+.. _LocalInterpretationRulesForNotations:
+
 Local interpretation rules for notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -897,7 +901,7 @@ Binding arguments of a constant to an interpretation scope
 .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes
 
    Defines extra argument scopes, to be used in case of coercion to Funclass
-   (see Chapter :ref:`Coercions-full`) or with a computed type.
+   (see Chapter :ref:`implicitcoercions`) or with a computed type.
 
 .. cmdv:: Global Arguments @qualid {+ @name%@scope}
 
@@ -957,7 +961,7 @@ Binding types of arguments to an interpretation scope
    type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted
    in scope ``scope``.
 
-   More generally, any coercion :n:`@class` (see Chapter :ref:`Coercions-full`)
+   More generally, any coercion :n:`@class` (see Chapter :ref:`implicitcoercions`)
    can be bound to an interpretation scope. The command to do it is
    :n:`Bind Scope @scope with @class`