[sphinx] Fix many warnings.

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

4 files changed, 58 insertions, 45 deletions

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
 -----------