[Sphinx] Fix all remaining warnings.

6 files changed, 96 insertions, 93 deletions

diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index fda20bff3..84810ddba 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -736,7 +736,7 @@ and this length is decremented for each rotation down to, but not
 including, 1 because for a list of length ``n``, we can make exactly
 ``n−1`` rotations to generate at most ``n`` distinct lists. Here, it
 must be noticed that we use the natural numbers of Coq for the
-rotation counter. On Figure :ref:`TODO-9.1-tactic-language`, we can
+rotation counter. In :ref:`ltac-syntax`, we can
 see that it is possible to use usual natural numbers but they are only
 used as arguments for primitive tactics and they cannot be handled, in
 particular, we cannot make computations with them. So, a natural
@@ -833,7 +833,7 @@ The pattern matching on goals allows a complete and so a powerful
 backtracking when returning tactic values. An interesting application
 is the problem of deciding intuitionistic propositional logic.
 Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff
-:ref:`TODO-56-biblio`, it is quite natural to code such a tactic
+:cite:`Dyc92`, it is quite natural to code such a tactic
 using the tactic language as shown on figures: :ref:`Deciding
 intuitionistic propositions (1) <decidingintuitionistic1>` and
 :ref:`Deciding intuitionistic propositions (2)
@@ -871,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, :cite:`TODO-45`). The axioms of this λ-calculus are given below.
+example, :cite:`RC95`). The axioms of this λ-calculus are given below.
 
 .. coqtop:: in reset
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 003d4b243..247d5d899 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -13,33 +13,34 @@ especially about its foundations, you can refer to :cite:`Del00`. Chapter
 :ref:`detailedexamplesoftactics` is devoted to giving examples of use of this
 language on small but also with non-trivial problems.
 
+.. _ltac-syntax:
+
 Syntax
 ------
 
-The syntax of the tactic language is given Figures :ref:`ltac, ltac_aux`. See
-Chapter :ref:`gallina` for a description of the BNF metasyntax used in these
-grammar rules. Various already defined entries will be used in this chapter:
-entries :token:`natural`, :token:`integer`, :token:`ident`, :token:`qualid`,
-:token:`term`, :token:`cpattern` and :token:`atomic_tactic` represent
-respectively the natural and integer numbers, the authorized identificators and
-qualified names, Coq terms and patterns and all the atomic tactics described in
-Chapter :ref:`tactics`. The syntax of :token:`cpattern` is the same as that of
-terms, but it is extended with pattern matching metavariables. In
-:token:`cpattern`, a pattern-matching metavariable is represented with the
-syntax :g:`?id` where :g:`id` is an :token:`ident`. The notation :g:`_` can also
-be used to denote metavariable whose instance is irrelevant. In the notation
-:g:`?id`, the identifier allows us to keep instantiations and to make
-constraints whereas :g:`_` shows that we are not interested in what will be
-matched. On the right hand side of pattern-matching clauses, the named
-metavariable are used without the question mark prefix. There is also a special
-notation for second-order pattern-matching problems: in an applicative pattern
-of the form :g:`@?id id1 … idn`, the variable id matches any complex expression
-with (possible) dependencies in the variables :g:`id1 … idn` and returns a
-functional term of the form :g:`fun id1 … idn => term`.
+The syntax of the tactic language is given below. See Chapter
+:ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used
+in these grammar rules. Various already defined entries will be used in this
+chapter: entries :token:`natural`, :token:`integer`, :token:`ident`,
+:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`atomic_tactic`
+represent respectively the natural and integer numbers, the authorized
+identificators and qualified names, Coq terms and patterns and all the atomic
+tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is
+the same as that of terms, but it is extended with pattern matching
+metavariables. In :token:`cpattern`, a pattern-matching metavariable is
+represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The
+notation :g:`_` can also be used to denote metavariable whose instance is
+irrelevant. In the notation :g:`?id`, the identifier allows us to keep
+instantiations and to make constraints whereas :g:`_` shows that we are not
+interested in what will be matched. On the right hand side of pattern-matching
+clauses, the named metavariable are used without the question mark prefix. There
+is also a special notation for second-order pattern-matching problems: in an
+applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any
+complex expression with (possible) dependencies in the variables :g:`id1 … idn`
+and returns a functional term of the form :g:`fun id1 … idn => term`.
 
 The main entry of the grammar is :n:`@expr`. This language is used in proof
-mode but it can also be used in toplevel definitions as shown in
-Figure :ref:`ltactop`.
+mode but it can also be used in toplevel definitions as shown below.
 
 .. note::
 
@@ -153,6 +154,8 @@ Figure :ref:`ltactop`.
    ltac_def         : `ident` [`ident` ... `ident`] := `expr`
                     : | `qualid` [`ident` ... `ident`] ::= `expr`
 
+.. _ltac-semantics:
+
 Semantics
 ---------
 
@@ -228,6 +231,8 @@ following form:
       independently. All the above variants work in this form too.
       Formally, :n:`@expr ; [ ... ]` is equivalent to :n:`[> @expr ; [> ... ] .. ]`.
 
+.. _goal-selectors:
+
 Goal selectors
 ~~~~~~~~~~~~~~
 
@@ -247,7 +252,7 @@ focused goals with:
    .. tacv:: [@ident] : @expr
 
       In this variant, :n:`@expr` is applied locally to a goal previously named
-      by the user (see :ref:`ExistentialVariables`).
+      by the user (see :ref:`existential-variables`).
 
    .. tacv:: @num : @expr
 
@@ -275,6 +280,9 @@ focused goals with:
       the toplevel of a tactic expression.
 
    .. exn:: No such goal
+      :name: No such goal (goal selector)
+
+   .. TODO change error message index entry
 
 For loop
 ~~~~~~~~
@@ -759,7 +767,7 @@ We can carry out pattern matching on terms with:
       matching subterm is tried. If no further subterm matches, the next clause
       is tried. Matching subterms are considered top-bottom and from left to
       right (with respect to the raw printing obtained by setting option
-      ``Printing All``, see Section :ref:`SetPrintingAll`).
+      :opt:`Printing All`).
 
    .. example::
 
@@ -775,6 +783,8 @@ We can carry out pattern matching on terms with:
          Goal True.
          f (3+4).
 
+.. _ltac-match-goal:
+
 Pattern matching on goals
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1009,6 +1019,7 @@ Proving a subgoal as a separate lemma
          don’t play well with asynchronous proofs.
 
    .. exn:: Proof is not complete
+      :name: Proof is not complete (abstract)
 
 Tactic toplevel definitions
 ---------------------------
@@ -1253,4 +1264,4 @@ Run-time optimization tactic
 
 This tactic behaves like :n:`idtac`, except that running it compacts the
 heap in the OCaml run-time system. It is analogous to the Vernacular
-command ``Optimize Heap`` (see :ref:`vernac-optimizeheap`).
+command :cmd:`Optimize Heap`.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index c28e85171..a77b127eb 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -20,20 +20,18 @@ prove. Initially, the list consists only in the theorem itself. After
 having applied some tactics, the list of goals contains the subgoals
 generated by the tactics.
 
-To each subgoal is associated a number of hypotheses called the *local
-context* of the goal. Initially, the local context contains the local
-variables and hypotheses of the current section (see Section :ref:`TODO_gallina_assumptions`)
-and the local variables and hypotheses of the theorem statement. It is
-enriched by the use of certain tactics (see e.g. ``intro`` in Section
-:ref:`managingthelocalcontext`).
+To each subgoal is associated a number of hypotheses called the *local context*
+of the goal. Initially, the local context contains the local variables and
+hypotheses of the current section (see Section :ref:`gallina-assumptions`) and
+the local variables and hypotheses of the theorem statement. It is enriched by
+the use of certain tactics (see e.g. :tacn:`intro`).
 
 When a proof is completed, the message ``Proof completed`` is displayed.
 One can then register this proof as a defined constant in the
 environment. Because there exists a correspondence between proofs and
-terms of λ-calculus, known as the *Curry-Howard isomorphism* [[How80]_,
-[Bar81]_, [Gir89]_, [Hue88]_ ], |Coq|
-stores proofs as terms of |Cic|. Those terms
-are called *proof terms*.
+terms of λ-calculus, known as the *Curry-Howard isomorphism*
+:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those
+terms are called *proof terms*.
 
 
 .. exn:: No focused proof
@@ -46,13 +44,10 @@ out of the proof editing mode.
 Switching on/off the proof editing mode
 -------------------------------------------
 
-The proof editing mode is entered by asserting a statement, which
-typically is the assertion of a theorem:
-
-.. cmd:: Theorem @ident [@binders] : @form.
-
-The list of assertion commands is given in Section :ref:TODO-assertions_and_proof`. The
-command ``Goal`` can also be used.
+The proof editing mode is entered by asserting a statement, which typically is
+the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
+list of assertion commands is given in Section :ref:`Assertions`. The command
+:cmd:`Goal` can also be used.
 
 .. cmd:: Goal @form.
 
@@ -95,14 +90,13 @@ Forces the name of the original goal to be :n:`@ident`. This
 command (and the following ones) can only be used if the original goal
 has been opened using the ``Goal`` command.
 
-
 .. cmd:: Admitted.
 
 This command is available in interactive editing proof mode to give up
 the current proof and declare the initial goal as an axiom.
 
-
 .. cmd:: Proof @term.
+   :name: Proof `term`
 
 This command applies in proof editing mode. It is equivalent to
 
@@ -127,7 +121,7 @@ See also: ``Proof with tactic.`` in Section
 .. cmd:: Proof using @ident1 ... @identn.
 
 This command applies in proof editing mode. It declares the set of
-section variables (see :ref:`TODO-gallina-assumptions`) used by the proof. At ``Qed`` time, the
+section variables (see :ref:`gallina-assumptions`) used by the proof. At ``Qed`` time, the
 system will assert that the set of section variables actually used in
 the proof is a subset of the declared one.
 
@@ -354,10 +348,10 @@ Error messages:
 You are trying to use ``}`` but the current subproof has not been fully solved.
 
 .. exn:: No such goal
+   :name: No such goal (focusing)
 
 .. exn:: Brackets only support the single numbered goal selector
 
-
 See also error messages about bullets below.
 
 .. _bullets:
@@ -597,4 +591,4 @@ the ongoing proof.
 This command forces the |OCaml| runtime to perform a heap compaction.
 This is in general an expensive operation.
 See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-There is also an analogous tactic ``optimize_heap`` (see~:ref:`tactic-optimizeheap`)
+There is also an analogous tactic :tac:`optimize_heap`.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index df5b36297..074c6f1e2 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5185,6 +5185,7 @@ equivalences are indeed taken into account, otherwise only single
 |SSR| proposes an extension of the Search command. Its syntax is:
 
 .. cmd:: Search {? @pattern }  {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } }
+   :name: Search (ssreflect)
 
 where :token:`qualid` is the name of an open module. This command returns
 the list of lemmas:
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 046efa730..08aa7110d 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -34,7 +34,7 @@ satisfied. If it is not the case, the tactic raises an error message.
 Tactics are built from atomic tactics and tactic expressions (which
 extends the folklore notion of tactical) to combine those atomic
 tactics. This chapter is devoted to atomic tactics. The tactic
-language will be described in Chapter :ref:`TODO-9-Thetacticlanguage`.
+language will be described in Chapter :ref:`ltac`.
 
 .. _invocation-of-tactics:
 
@@ -42,7 +42,7 @@ 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
+goal selector (see Section :ref:`ltac-semantics`). If no selector is
 specified, the default selector is used.
 
 .. _tactic_invocation_grammar:
@@ -95,7 +95,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
 + A bindings list can also be a simple list of terms :n:`{* term}`.
   In that case the references to which these terms correspond are
   determined by the tactic. In case of ``induction``, ``destruct``, ``elim``
-  and ``case`` (see :ref:`TODO-9-Thetacticlanguage`) the terms have to
+  and ``case`` (see :ref:`ltac`) the terms have to
   provide instances for all the dependent products in the type of term while in
   the case of ``apply``, or of ``constructor`` and its variants, only instances
   for the dependent products that are not bound in the conclusion of the type
@@ -279,7 +279,7 @@ gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...`  :g:`u`:sub:`n`.
 
 The apply tactic failed to match the conclusion of term and the current goal.
 You can help the apply tactic by transforming your goal with the
-:ref:`change <change_term>` or :tacn:`pattern` tactics.
+:tacn:`change` or :tacn:`pattern` tactics.
 
 .. exn:: Unable to find an instance for the variables {+ @ident}.
 
@@ -287,7 +287,7 @@ This occurs when some instantiations of the premises of term are not deducible
 from the unification. This is the case, for instance, when you want to apply a
 transitivity property. In this case, you have to use one of the variants below:
 
-.. cmd:: apply @term with {+ @term}
+.. tacv:: apply @term with {+ @term}
 
 Provides apply with explicit instantiations for all dependent premises of the
 type of term that do not occur in the conclusion and consequently cannot be
@@ -1091,7 +1091,7 @@ Controlling the proof flow
 
 .. tacv:: assert form
 
-   This behaves as :n:`assert (@ident : form ) but :n:`@ident` is generated by
+   This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by
    Coq.
 
 .. tacv:: assert form by tactic
@@ -1100,6 +1100,7 @@ Controlling the proof flow
    generated by assert.
 
    .. exn:: Proof is not complete
+      :name: Proof is not complete (assert)
 
 .. tacv:: assert form as intro_pattern
 
@@ -1750,7 +1751,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    results equivalent to ``inversion`` or ``dependent inversion`` if the
    hypothesis is dependent.
 
-See also :ref:`dependentinduction` for a larger example of ``dependent induction``
+See also the larger example of :tacn:`dependent induction`
 and an explanation of the underlying technique.
 
 .. tacn:: function induction (@qualid {+ @term})
@@ -2910,7 +2911,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This tactic applies to any goal. The argument qualid must denote a
    defined transparent constant or local definition (see
-   :ref:`TODO-1.3.2-Definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic
+   :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic
    ``unfold`` applies the :math:`\delta` rule to each occurrence of the constant to which
    :n:`@qualid` refers in the current goal and then replaces it with its
    :math:`\beta`:math:`\iota`-normal form.
@@ -3608,40 +3609,37 @@ Setting implicit automation tactics
    In this case the tactic command typed by the user is equivalent to
    ``tactic``:sub:`1` ``;tactic``.
 
-See also: ``Proof.`` in :ref:`proof-editing-mode`.
+   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:`proof-editing-mode`
+   .. cmdv:: Proof with tactic using {+ @ident}
 
-.. cmd:: Proof using {+ @ident} with tactic
+      Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
-   Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
+   .. cmdv:: Proof using {+ @ident} with tactic
 
-.. cmd:: Declare Implicit Tactic tactic
+      Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
-   This command declares a tactic to be used to solve implicit arguments
-   that Coq does not know how to solve by unification. It is used every
-   time the term argument of a tactic has one of its holes not fully
-   resolved.
+   .. cmd:: Declare Implicit Tactic tactic
 
-Here is an example:
+      This command declares a tactic to be used to solve implicit arguments
+      that Coq does not know how to solve by unification. It is used every
+      time the term argument of a tactic has one of its holes not fully
+      resolved.
 
-.. example::
+   .. example::
 
-   .. coqtop:: all
+      .. coqtop:: all
 
-      Parameter quo : nat -> forall n:nat, n<>0 -> nat.
-      Notation "x // y" := (quo x y _) (at level 40).
-      Declare Implicit Tactic assumption.
-      Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
-      intros.
-      exists (n // m).
+         Parameter quo : nat -> forall n:nat, n<>0 -> nat.
+         Notation "x // y" := (quo x y _) (at level 40).
+         Declare Implicit Tactic assumption.
+         Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
+         intros.
+         exists (n // m).
 
-   The tactic ``exists (n // m)`` did not fail. The hole was solved
-   by ``assumption`` so that it behaved as ``exists (quo n m H)``.
+      The tactic ``exists (n // m)`` did not fail. The hole was solved
+      by ``assumption`` so that it behaved as ``exists (quo n m H)``.
 
 .. _decisionprocedures:
 
@@ -3719,7 +3717,7 @@ and then uses :tacn:`auto` which completes the proof.
 
 Originally due to César Muñoz, these tactics (:tacn:`tauto` and
 :tacn:`intuition`) have been completely re-engineered by David Delahaye using
-mainly the tactic language (see :ref:`TODO-9-thetacticlanguage`). The code is
+mainly the tactic language (see :ref:`ltac`). The code is
 now much shorter and a significant increase in performance has been noticed.
 The general behavior with respect to dependent types, unfolding and
 introductions has slightly changed to get clearer semantics. This may lead to
@@ -4346,7 +4344,7 @@ close the section (see also :ref:`section-mechanism`) where it was
 defined. If you want that a tactic macro defined in a module is usable in the
 modules that require it, you should put it outside of any section.
 
-:ref:`TODO-9-Thetacticlanguage` gives examples of more complex
+:ref:`ltac` gives examples of more complex
 user-defined tactics.
 
 .. [1] Actually, only the second subgoal will be generated since the
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index f7693d551..da4034fb8 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1393,16 +1393,15 @@ scope of their effect. There are four kinds of commands:
   (see Section :ref:`coercions`) and ``Strategy`` (see :ref:`here <vernac-strategy>`)
   commands belong to this category.
 + Commands whose default behavior is to stop their effect at the end
-  of the section they occur in but to extent their effect outside the
-  module or library file they occur in.  For these commands, the Local
-  modifier limits the effect of the command to the current module if the
-  command does not occur in a section and the Global modifier extends
-  the effect outside the current sections and current module if the
-  command occurs in a section.  As an example, the ``Implicit Arguments`` (see
-  Section :ref:`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.
+  of the section they occur in but to extent their effect outside the module or
+  library file they occur in. For these commands, the Local modifier limits the
+  effect of the command to the current module if the command does not occur in a
+  section and the Global modifier extends the effect outside the current
+  sections and current module if the command occurs in a section. As an example,
+  the :cmd:`Implicit Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
+  to this category. Notice that a subclass of these commands do not support
+  extension of their scope outside sections at all and the Global is not
+  applicable to them.
 + Commands whose default behavior is to stop their effect at the end
   of the section or module they occur in.  For these commands, the Global
   modifier extends their effect outside the sections and modules they