[sphinx] Fix many warnings.

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

1 files changed, 59 insertions, 51 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2af73c28e5..046efa7307 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.