[sphinx] Fix many warnings.

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

8 files changed, 60 insertions, 66 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