[Sphinx] Fix all remaining warnings.

6 files changed, 33 insertions, 35 deletions

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 64d4eddf0..1d3b66173 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -305,6 +305,8 @@ explicitations (as for terms 2.7.11).
         end).
 
 
+.. _matching-dependent:
+
 Matching objects of dependent types
 -----------------------------------
 
@@ -414,6 +416,7 @@ length, by writing
 
 I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`.
 
+.. _match-in-patterns:
 
 Patterns in ``in``
 ~~~~~~~~~~~~~~~~~~
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 0e72c996f..d60387f4f 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -707,20 +707,18 @@ 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:`TypeclassesTransparent`).
 
-
 Strategies for rewriting
 ------------------------
 
-
 Definitions
 ~~~~~~~~~~~
 
-The generalized rewriting tactic is based on a set of strategies that
-can be combined to obtain custom rewriting procedures. Its set of
-strategies is based on Elan’s rewriting strategies :ref:`TODO-102-biblio`. Rewriting
+The generalized rewriting tactic is based on a set of strategies that can be
+combined to obtain custom rewriting procedures. Its set of strategies is based
+on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting
 strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a
-strategy expression. Strategies are defined inductively as described
-by the following grammar:
+strategy expression. Strategies are defined inductively as described by the
+following grammar:
 
 .. productionlist:: rewriting
    s, t, u : `strategy`
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 68e071d7c..ec1b942e0 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -272,25 +272,24 @@ Activating the Printing of Coercions
 Classes as Records
 ------------------
 
-We allow the definition of *Structures with Inheritance* (or
-classes as records) by extending the existing ``Record`` macro
-(see Section :ref:`record-types`). Its new syntax is:
-
-.. cmd:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
-
-  The first identifier `ident` is the name of the defined record and
-  `sort` is its type. The optional identifier after ``:=`` is the name
-  of the constuctor (it will be ``Build_``\ `ident` if not given).
-  The other identifiers are the names of the fields, and the `term`
-  are their respective types. If ``:>`` is used instead of ``:`` in
-  the declaration of a field, then the name of this field is automatically
-  declared as a coercion from the record name to the class of this
-  field type. Remark that the fields always verify the uniform
-  inheritance condition. If the optional ``>`` is given before the
-  record name, then the constructor name is automatically declared as
-  a coercion from the class of the last field type to the record name
-  (this may fail if the uniform inheritance condition is not
-  satisfied).
+We allow the definition of *Structures with Inheritance* (or classes as records)
+by extending the existing :cmd:`Record` macro. Its new syntax is:
+
+.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
+
+   The first identifier `ident` is the name of the defined record and
+   `sort` is its type. The optional identifier after ``:=`` is the name
+   of the constuctor (it will be ``Build_``\ `ident` if not given).
+   The other identifiers are the names of the fields, and the `term`
+   are their respective types. If ``:>`` is used instead of ``:`` in
+   the declaration of a field, then the name of this field is automatically
+   declared as a coercion from the record name to the class of this
+   field type. Remark that the fields always verify the uniform
+   inheritance condition. If the optional ``>`` is given before the
+   record name, then the constructor name is automatically declared as
+   a coercion from the class of the last field type to the record name
+   (this may fail if the uniform inheritance condition is not
+   satisfied).
 
 .. note::
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index a2940881d..1c3fdeb43 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -135,8 +135,7 @@ 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 :ref:`gallina_def`) and Fixpoint
-(see Section :ref:`TODO-1.3.4-Fixpoint`)
+:cmd:`Definition` and :cmd:`Fixpoint`
 in that they define constants. However, they may require the user to
 prove some goals to construct the final definitions.
 
@@ -197,7 +196,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 :ref:`TODO-1.3.4-Fixpoint`), except it may also generate obligations. It works
+:cmd:`Fixpoint`), except it may also generate obligations. It works
 with mutually recursive definitions too.
 
 .. coqtop:: reset none
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index b861892cb..ae666a0d4 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -701,7 +701,7 @@ for |Coq|’s type-checker. Let us see why:
 At each step of rewriting, the whole context is duplicated in the
 proof term. Then, a tactic that does hundreds of rewriting generates
 huge proof terms. Since ``ACDSimpl`` was too slow, Samuel Boutin rewrote
-it using reflection (see his article in TACS’97 [Bou97]_). Later, it
+it using reflection (see :cite:`Bou97`). Later, it
 was rewritten by Patrick Loiseleur: the new tactic does not any
 more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not
 only to replace the rewriting steps, but also to achieve the
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index add03b946..8861cac8a 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -148,11 +148,10 @@ database.
 Sections and contexts
 ---------------------
 
-To ease the parametrization of developments by type classes, we
-provide a new way to introduce variables into section contexts,
-compatible with the implicit argument mechanism. The new command works
-similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it
-accepts any binding context as argument. For example:
+To ease the parametrization of developments by type classes, we provide a new
+way to introduce variables into section contexts, compatible with the implicit
+argument mechanism. The new command works similarly to the :cmd:`Variables`
+vernacular, except it accepts any binding context as argument. For example:
 
 .. coqtop:: all