[Sphinx] Fix all remaining warnings.

4 files changed, 162 insertions, 125 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 839f3ce56..5a2aa0a1f 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -401,9 +401,11 @@ can decide if two programs are *intentionally* equal (one says
 *convertible*). Convertibility is described in this section.
 
 
-.. _β-reduction:
+.. _beta-reduction:
+
+β-reduction
+~~~~~~~~~~~
 
-**β-reduction.**
 We want to be able to identify some terms as we can identify the
 application of a function to a given argument with its result. For
 instance the identity function over a given type T can be written
@@ -427,9 +429,11 @@ theoretically of great importance but we will not detail them here and
 refer the interested reader to :cite:`Coq85`.
 
 
-.. _ι-reduction:
+.. _iota-reduction:
+
+ι-reduction
+~~~~~~~~~~~
 
-**ι-reduction.**
 A specific conversion rule is associated to the inductive objects in
 the global environment. We shall give later on (see Section
 :ref:`Well-formed-inductive-definitions`) the precise rules but it
@@ -438,9 +442,11 @@ constructor behaves as expected. This reduction is called ι-reduction
 and is more precisely studied in :cite:`Moh93,Wer94`.
 
 
-.. _δ-reduction:
+.. _delta-reduction:
+
+δ-reduction
+~~~~~~~~~~~
 
-**δ-reduction.**
 We may have variables defined in local contexts or constants defined
 in the global environment. It is legal to identify such a reference
 with its value, that is to expand (or unfold) it into its value. This
@@ -461,9 +467,11 @@ reduction is called δ-reduction and shows as follows.
    E[Γ] ⊢ c~\triangleright_δ~t
 
 
-.. _ζ-reduction:
+.. _zeta-reduction:
+
+ζ-reduction
+~~~~~~~~~~~
 
-**ζ-reduction.**
 |Coq| allows also to remove local definitions occurring in terms by
 replacing the defined variable by its value. The declaration being
 destroyed, this reduction differs from δ-reduction. It is called
@@ -478,9 +486,11 @@ destroyed, this reduction differs from δ-reduction. It is called
    E[Γ] ⊢ \letin{x}{u}{t}~\triangleright_ζ~\subst{t}{x}{u}
 
 
-.. _η-expansion:
+.. _eta-expansion:
+
+η-expansion
+~~~~~~~~~~~
 
-**η-expansion.**
 Another important concept is η-expansion. It is legal to identify any
 term :math:`t` of functional type :math:`∀ x:T, U` with its so-called η-expansion
 
@@ -517,9 +527,11 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`.
    convertible to the type of the original term :math:`∀ x:\Type(1),\Type(1).`
 
 
-.. _Convertibility:
+.. _convertibility:
+
+Convertibility
+~~~~~~~~~~~~~~
 
-**Convertibility.**
 Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the
 relation :math:`t` reduces to :math:`u` in the global environment
 :math:`E` and local context :math:`Γ` with one of the previous
@@ -823,8 +835,9 @@ to inconsistent systems. We restrict ourselves to definitions which
 satisfy a syntactic criterion of positivity. Before giving the formal
 rules, we need a few definitions:
 
+Arity of a given sort
++++++++++++++++++++++
 
-**Type is an Arity of Sort S.**
 A type :math:`T` is an *arity of sort s* if it converts to the sort s or to a
 product :math:`∀ x:T,U` with :math:`U` an arity of sort s.
 
@@ -834,7 +847,8 @@ product :math:`∀ x:T,U` with :math:`U` an arity of sort s.
    :math:`\Prop`.
 
 
-**Type is an Arity.**
+Arity
++++++
 A type :math:`T` is an *arity* if there is a :math:`s∈ \Sort` such that :math:`T` is an arity of
 sort s.
 
@@ -844,32 +858,34 @@ sort s.
    :math:`A→ Set` and :math:`∀ A:\Prop,A→ \Prop` are arities.
 
 
-**Type of Constructor of I.**
+Type constructor
+++++++++++++++++
 We say that T is a *type of constructor of I* in one of the following
 two cases:
 
-
 + :math:`T` is :math:`(I~t_1 … t_n )`
 + :math:`T` is :math:`∀ x:U,T'` where :math:`T'` is also a type of constructor of :math:`I`
 
-
-
 .. example::
 
    :math:`\nat` and :math:`\nat→\nat` are types of constructor of :math:`\nat`.
    :math:`∀ A:Type,\List~A` and :math:`∀ A:Type,A→\List~A→\List~A` are types of constructor of :math:`\List`.
 
-**Positivity Condition.**
+.. _positivity:
+
+Positivity Condition
+++++++++++++++++++++
+
 The type of constructor :math:`T` will be said to *satisfy the positivity
 condition* for a constant :math:`X` in the following cases:
 
-
 + :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i`
 + :math:`T=∀ x:U,V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V`
   satisfies the positivity condition for :math:`X`.
-
   
-**Occurs Strictly Positively.**
+Strict positivity
++++++++++++++++++
+
 The constant :math:`X` *occurs strictly positively* in :math:`T` in the following
 cases:
 
@@ -889,11 +905,12 @@ cases:
   any of the :math:`t_i`, and the (instantiated) types of constructor
   :math:`\subst{C_i}{p_j}{a_j}_{j=1… m}` of :math:`I` satisfy the nested positivity condition for :math:`X`
 
-**Nested Positivity Condition.**
+Nested Positivity
++++++++++++++++++
+
 The type of constructor :math:`T` of :math:`I` *satisfies the nested positivity
 condition* for a constant :math:`X` in the following cases:
 
-
 + :math:`T=(I~b_1 … b_m~u_1 … u_p)`, :math:`I` is an inductive definition with :math:`m`
   parameters and :math:`X` does not occur in any :math:`u_i`
 + :math:`T=∀ x:U,V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V`
@@ -940,12 +957,11 @@ For instance, if one considers the type
            │
            ╰─ list satisfies the positivity condition for list A ... (bullet 1)
 
-
-
-
 .. _Correctness-rules:
 
-**Correctness rules.**
+Correctness rules
++++++++++++++++++
+
 We shall now describe the rules allowing the introduction of a new
 inductive definition.
 
@@ -1012,7 +1028,9 @@ has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`.
 
 .. _Template-polymorphism:
 
-**Template polymorphism.**
+Template polymorphism
++++++++++++++++++++++
+
 Inductive types declared in Type are polymorphic over their arguments
 in Type. If :math:`A` is an arity of some sort and s is a sort, we write :math:`A_{/s}`
 for the arity obtained from :math:`A` by replacing its sort with s.
@@ -1217,9 +1235,11 @@ Coquand in :cite:`Coq92`. One is the definition by pattern-matching. The
 second one is a definition by guarded fixpoints.
 
 
-.. _The-match…with-end-construction:
+.. _match-construction:
+
+The match ... with ... end construction
++++++++++++++++++++++++++++++++++++++++
 
-**The match…with …end construction**
 The basic idea of this operator is that we have an object :math:`m` in an
 inductive type :math:`I` and we want to prove a property which possibly
 depends on :math:`m`. For this, it is enough to prove the property for
@@ -1623,9 +1643,8 @@ Given a variable :math:`y` of type an inductive definition in a declaration
   ones in which one of the :math:`I_l` occurs) are structurally smaller than y.
 
 
-The following definitions are correct, we enter them using the ``Fixpoint``
-command as described in Section :ref:`TODO-1.3.4` and show the internal
-representation.
+The following definitions are correct, we enter them using the :cmd:`Fixpoint`
+command and show the internal representation.
 
 .. example::
    .. coqtop:: all
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index c5da866b8..6af6e7897 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -48,6 +48,7 @@ at the |Coq| root directory; this includes the modules
 ``Tactics``.
 Module ``Logic_Type`` also makes it in the initial state.
 
+.. _init-notations:
 
 Notations
 ~~~~~~~~~
@@ -929,9 +930,8 @@ tactics (see Chapter :ref:`tactics`), there are also:
     Goal forall x y z:R, x * y * z <> 0.
     intros; split_Rmult.
 
-These tactics has been written with the tactic language Ltac
-described in Chapter :ref:`thetacticlanguage`.
-
+These tactics has been written with the tactic language |Ltac|
+described in Chapter :ref:`ltac`.
 
 List library
 ~~~~~~~~~~~~
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ce10c651a..f474eade7 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -193,9 +193,9 @@ other arguments are the parameters of the inductive type.
   This message is followed by an explanation of this impossibility.
   There may be three reasons:
 
-  #. The name `ident` already exists in the environment (see Section :ref:`TODO-1.3.1-axioms`).
+  #. The name `ident` already exists in the environment (see :cmd:`Axiom`).
   #. The body of `ident` uses an incorrect elimination for
-     `ident` (see Sections :ref:`TODO-1.3.4-fixpoint` and :ref:`Destructors`).
+     `ident` (see :cmd:`Fixpoint` and :ref:`Destructors`).
   #. The type of the projections `ident` depends on previous
      projections which themselves could not be defined.
 
@@ -212,7 +212,7 @@ other arguments are the parameters of the inductive type.
 
 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.
+:ref:`gallina-inductive-definitions`, may also occur.
 
 **See also** Coercions and records in Section :ref:`coercions-classes-as-records` of the chapter devoted to coercions.
 
@@ -316,7 +316,7 @@ printed back as :g:`match` constructs.
 Variants and extensions of :g:`match`
 -------------------------------------
 
-.. _extended pattern-matching:
+.. _mult-match:
 
 Multiple and nested pattern-matching
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -330,8 +330,9 @@ into a sequence of match on simple patterns. Especially, a
 construction defined using the extended match is generally printed
 under its expanded form (see ``Set Printing Matching`` in :ref:`controlling-match-pp`).
 
-See also: :ref:`extended pattern-matching`.
+See also: :ref:`extendedpatternmatching`.
 
+.. _if-then-else:
 
 Pattern-matching on boolean values: the if expression
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -722,7 +723,7 @@ used by ``Function``. A more precise description is given below.
    the following are defined:
 
     + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern
-      matching structure of `term` (see the documentation of :ref:`TODO-1.3.3-Inductive`);
+      matching structure of `term` (see :cmd:`Inductive`);
     + The inductive `R_ident` corresponding to the graph of `ident` (silently);
     + `ident_complete` and `ident_correct` which are inversion information
       linking the function and its graph.
@@ -778,7 +779,7 @@ Section mechanism
 
 The sectioning mechanism can be used to to organize a proof in
 structured sections. Then local declarations become available (see
-Section :ref:`TODO-1.3.2-Definitions`).
+Section :ref:`gallina-definitions`).
 
 
 .. cmd:: Section @ident.
@@ -1240,10 +1241,6 @@ qualified name.
     This option (off by default) disables the printing of the types of fields,
     leaving only their names, for the commands ``Print Module`` and ``Print Module Type``.
 
-.. cmd:: Locate Module @qualid.
-
-    Prints the full name of the module `qualid`.
-
 Libraries and qualified names
 ---------------------------------
 
@@ -1256,7 +1253,7 @@ The theories developed in |Coq| are stored in *library files* which are
 hierarchically classified into *libraries* and *sublibraries*. To
 express this hierarchy, library names are represented by qualified
 identifiers qualid, i.e. as list of identifiers separated by dots (see
-:ref:`TODO-1.2.3-identifiers`). For instance, the library file ``Mult`` of the standard
+:ref:`gallina-identifiers`). For instance, the library file ``Mult`` of the standard
 |Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts
 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
@@ -1300,13 +1297,13 @@ 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:`compiled-files`), ``Import`` and ``Export`` (see :ref:`here <import_qualid>`) and
+commands :cmd:`Require`, :cmd:`Import` and :cmd:`Export` 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
 short or partially qualified name is mapped to the absolute name in
 |Coq| name table. Definitions flagged as Local are only accessible with
-their fully qualified name (see :ref:`TODO-1.3.2-definitions`).
+their fully qualified name (see :ref:`gallina-definitions`).
 
 It may happen that a visible name is hidden by the short name or a
 qualified name of another construction. In this case, the name that
@@ -1328,8 +1325,7 @@ accessible, absolute names can never be hidden.
 
        Locate nat.
 
-See also: Command Locate in :ref:`TODO-6.3.10-locate-qualid` and Locate Library in
-:ref:`TODO-6.6.11-locate-library`.
+See also: Commands :cmd:`Locate` and :cmd:`Locate Library`.
 
 .. _libraries-and-filesystem:
 
@@ -1589,6 +1585,7 @@ Declaring Implicit Arguments
 To set implicit arguments *a posteriori*, one can use the command:
 
 .. cmd:: Arguments @qualid {* @possibly_bracketed_ident }.
+   :name: Arguments (implicits)
 
 where the list of `possibly_bracketed_ident` is a prefix of the list of
 arguments of `qualid` where the ones to be declared implicit are
@@ -1802,6 +1799,8 @@ declares implicit arguments to be automatically inserted when a
 function is partially applied and the next argument of the function is
 an implicit one.
 
+.. _explicit-applications:
+
 Explicit applications
 ~~~~~~~~~~~~~~~~~~~~~
 
@@ -2147,16 +2146,17 @@ Printing universes
 
 .. opt:: Printing Universes.
 
-Turn this option on to activate the display of the actual level of each occurrence of ``Type``.
-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.
+Turn this option on to activate the display of the actual level of each
+occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in
+combination with :opt:`Printing All` 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:`Sorts`) can be printed using the command
 
 .. cmd:: Print {? Sorted} Universes.
+   :name: Print Universes
 
 If the optional ``Sorted`` option is given, each universe will be made
 equivalent to a numbered label reflecting its level (with a linear
@@ -2164,7 +2164,7 @@ ordering) in the universe hierarchy.
 
 This command also accepts an optional output filename:
 
-.. cmd:: Print {? Sorted} Universes @string.
+.. cmdv:: Print {? Sorted} Universes @string.
 
 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
@@ -2227,7 +2227,7 @@ existential variable used in the same context as its context of definition is wr
 Existential variables can be named by the user upon creation using
 the syntax ``?``\ `ident`. This is useful when the existential
 variable needs to be explicitly handled later in the script (e.g.
-with a named-goal selector, see :ref:`TODO-9.2-goal-selectors`).
+with a named-goal selector, see :ref:`goal-selectors`).
 
 .. _explicit-display-existentials:
 
@@ -2252,7 +2252,7 @@ is not specified and is implementation-dependent. The inner tactic may
 use any variable defined in its scope, including repeated alternations
 between variables introduced by term binding as well as those
 introduced by tactic binding. The expression `tacexpr` can be any tactic
-expression as described in :ref:`thetacticlanguage`.
+expression as described in :ref:`ltac`.
 
 .. coqtop:: all
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 6458ceeaa..246f45b3e 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1,4 +1,4 @@
-.. _BNF-syntax:
+.. _gallinaspecificationlanguage:
 
 ------------------------------------
  The Gallina specification language
@@ -188,6 +188,8 @@ Coq terms are typed. Coq types are recognized by the same syntactic
 class as :token`term`. We denote by :token:`type` the semantic subclass
 of types inside the syntactic class :token:`term`.
 
+.. _gallina-identifiers:
+
 Qualified identifiers and simple identifiers
 --------------------------------------------
 
@@ -230,6 +232,8 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`.
 
 More on sorts can be found in Section :ref:`sorts`.
 
+.. _binders:
+
 Binders
 -------
 
@@ -312,7 +316,7 @@ left.
 
 The notation ``(ident := term)`` for arguments is used for making
 explicit the value of implicit arguments (see
-Section :ref:`Implicits-explicitation`).
+Section :ref:`explicit-applications`).
 
 Type cast
 ---------
@@ -330,6 +334,8 @@ Expressions often contain redundant pieces of information. Subterms that can be
 automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will
 guess the missing piece of information.
 
+.. _let-in:
+
 Let-in definitions
 ------------------
 
@@ -350,7 +356,7 @@ expression is used to analyze the structure of an inductive objects and
 to apply specific treatments accordingly.
 
 This paragraph describes the basic form of pattern-matching. See
-Section :ref:`Mult-match` and Chapter :ref:`Mult-match-full` for the description
+Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
 of the general form. The basic form of pattern-matching is characterized
 by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a
 single :token:`pattern` and :token:`pattern` restricted to the form
@@ -417,7 +423,7 @@ accepted and has the same meaning as the previous one.
 The second subcase is only relevant for annotated inductive types such
 as the equality predicate (see Section :ref:`Equality`),
 the order predicate on natural numbers or the type of lists of a given
-length (see Section :ref:`listn`). In this configuration, the
+length (see Section :ref:`matching-dependent`). In this configuration, the
 type of each branch can depend on the type dependencies specific to the
 branch and the whole pattern-matching expression has a type determined
 by the specific dependencies in the type of the term being matched. This
@@ -460,18 +466,17 @@ in are available.
 
 There are specific notations for case analysis on types with one or two
 constructors: “if … then … else …” and “let (…, ” (see
-Sections :ref:`if-then-else` and :ref:`Letin`).
+Sections :ref:`if-then-else` and :ref:`let-in`).
 
 Recursive functions
 -------------------
 
 The expression “fix :token:`ident`:math:`_1` :token:`binder`:math:`_1` :
 :token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` with … with
-:token:`ident`:math:`_n` :token:`binder`:math:`_n` : :token:`type`:math:`_n` ``:=``
-:token:`term`:math:`_n` for :token:`ident`:math:`_i`” denotes the
-:math:`i`\ component of a block of functions defined by mutual
-well-founded recursion. It is the local counterpart of the ``Fixpoint``
-command. See Section :ref:`Fixpoint` for more details. When
+:token:`ident`:math:`_n` :token:`binder`:math:`_n` : :token:`type`:math:`_n`
+``:=`` :token:`term`:math:`_n` for :token:`ident`:math:`_i`” denotes the
+:math:`i`\ component of a block of functions defined by mutual well-founded
+recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When
 :math:`n=1`, the “for :token:`ident`:math:`_i`” clause is omitted.
 
 The expression “cofix :token:`ident`:math:`_1` :token:`binder`:math:`_1` :
@@ -531,6 +536,8 @@ dot.
 The different kinds of command are described hereafter. They all suppose
 that the terms occurring in the sentences are well-typed.
 
+.. _gallina-assumptions:
+
 Assumptions
 -----------
 
@@ -542,6 +549,8 @@ the same module. This :token:`type` is considered to be the type (or
 specification, or statement) assumed by :token:`ident` and we say that :token:`ident`
 has type :token:`type`.
 
+.. _Axiom:
+
 .. cmd:: Axiom @ident : @term.
 
    This command links *term* to the name *ident* as its specification in
@@ -568,10 +577,9 @@ has type :token:`type`.
 
 .. cmdv:: Local Axiom @ident : @term.
 
-   Such axioms are never made accessible through their unqualified
-   name by ``Import`` and its variants (see :ref:`Import`). You
-   have to explicitly give their fully qualified name to refer to
-   them.
+   Such axioms are never made accessible through their unqualified name by
+   :cmd:`Import` and its variants. You have to explicitly give their fully
+   qualified name to refer to them.
 
 .. cmdv:: Conjecture @ident : @term
 
@@ -580,11 +588,11 @@ has type :token:`type`.
 .. cmd:: Variable @ident : @term.
 
 This command links :token:`term` to the name :token:`ident` in the context of
-the current section (see Section :ref:`Section` for a description of the section
-mechanism). When the current section is closed, name :token:`ident` will be
-unknown and every object using this variable will be explicitly parametrized
-(the variable is *discharged*). Using the ``Variable`` command out of any
-section is equivalent to using ``Local Parameter``.
+the current section (see Section :ref:`section-mechanism` for a description of
+the section mechanism). When the current section is closed, name :token:`ident`
+will be unknown and every object using this variable will be explicitly
+parametrized (the variable is *discharged*). Using the ``Variable`` command out
+of any section is equivalent to using ``Local Parameter``.
 
 .. exn:: @ident already exists
 
@@ -609,7 +617,7 @@ 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:
+.. _gallina-definitions:
 
 Definitions
 -----------
@@ -620,7 +628,7 @@ way to abbreviate a term. In any case, the name can later be replaced at
 any time by its definition.
 
 The operation of unfolding a name into its definition is called
-:math:`\delta`-conversion (see Section :ref:`delta`). A
+:math:`\delta`-conversion (see Section :ref:`delta-reduction`). A
 definition is accepted by the system if and only if the defined term is
 well-typed in the current context of the definition and if the name is
 not already used. The name defined by the definition is called a
@@ -628,7 +636,7 @@ not already used. The name defined by the definition is called a
 type which is the type of its body.
 
 A formal presentation of constants and environments is given in
-Section :ref:`Typed-terms`.
+Section :ref:`typing-rules`.
 
 .. cmd:: Definition @ident := @term.
 
@@ -654,7 +662,7 @@ Section :ref:`Typed-terms`.
 .. cmdv:: Local Definition @ident := @term.
 
    Such definitions are never made accessible through their
-   unqualified name by Import and its variants (see :ref:`Import`).
+   unqualified name by :cmd:`Import` and its variants.
    You have to explicitly give their fully qualified name to refer to them.
 
 .. cmdv:: Example @ident := @term.
@@ -667,7 +675,7 @@ These are synonyms of the Definition forms.
 
 .. exn:: The term @term has type @type while it is expected to have type @type
 
-See also Sections :ref:`Opaque,Transparent,unfold`.
+See also :cmd:`Opaque`, :cmd:`Transparent`, :tac:`unfold`.
 
 .. cmd:: Let @ident := @term.
 
@@ -687,7 +695,10 @@ prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term`
 
 .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}.
 
-See also Sections :ref:`Section,Opaque,Transparent,unfold`.
+See also Sections :ref:`section-mechanism`, commands :cmd:`Opaque`,
+:cmd:`Transparent`, and tactic :tacn:`unfold`.
+
+.. _gallina-inductive-definitions:
 
 Inductive definitions
 ---------------------
@@ -707,7 +718,7 @@ The name :token:`ident` is the name of the inductively defined type and
 :token:`sort` is the universes where it lives. The :token:`ident` are the names
 of its constructors and :token:`type` their respective types. The types of the
 constructors have to satisfy a *positivity condition* (see Section
-:ref:`Positivity`) for :token:`ident`. This condition ensures the soundness of
+:ref:`positivity`) for :token:`ident`. This condition ensures the soundness of
 the inductive definition. If this is the case, the :token:`ident` are added to
 the environment with their respective types. Accordingly to the universe where
 the inductive type lives (e.g. its type :token:`sort`), Coq provides a number of
@@ -848,8 +859,7 @@ arguments of the constructors rather than their full type.
 The ``Variant`` keyword is identical to the ``Inductive`` keyword, except
 that it disallows recursive definition of types (in particular lists cannot
 be defined with the Variant keyword). No induction scheme is generated for
-this variant, unless the option ``Nonrecursive Elimination Schemes`` is set
-(see :ref:`set-nonrecursive-elimination-schemes`).
+this variant, unless :opt:`Nonrecursive Elimination Schemes` is set.
 
 .. exn:: The @num th argument of @ident must be @ident in @type
 
@@ -891,7 +901,8 @@ instead of parameters but it will sometimes give a different (bigger)
 sort for the inductive definition and will produce a less convenient
 rule for case elimination.
 
-See also Sections :ref:`Cic-inductive-definitions,Tac-induction`.
+See also Section :ref:`inductive-definitions` and the :tacn:`induction`
+tactic.
 
 Mutually defined inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -960,7 +971,9 @@ section is closed, the variables declared in the section and occurring
 free in the declaration are added as parameters to the inductive
 definition.
 
-See also Section :ref:`Section`.
+See also Section :ref:`section-mechanism`.
+
+.. _coinductive-types:
 
 Co-inductive types
 ~~~~~~~~~~~~~~~~~~
@@ -982,12 +995,12 @@ Coq using the ``CoInductive`` command:
    CoInductive Stream : Set :=
      Seq : nat -> Stream -> Stream.
 
-The syntax of this command is the same as the command ``Inductive`` (see
-Section :ref:`gal-Inductive-Definitions`. Notice that no principle of induction
-is derived from the definition of a co-inductive type, since such principles
-only make sense for inductive ones. For co-inductive ones, the only elimination
-principle is case analysis. For example, the usual destructors on streams
-:g:`hd:Stream->nat` and :g:`tl:Str->Str` can be defined as follows:
+The syntax of this command is the same as the command :cmd:`Inductive`. Notice
+that no principle of induction is derived from the definition of a co-inductive
+type, since such principles only make sense for inductive ones. For co-inductive
+ones, the only elimination principle is case analysis. For example, the usual
+destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` can be defined
+as follows:
 
 .. coqtop:: all
 
@@ -1007,7 +1020,7 @@ predicate is the extensional equality on streams:
 In order to prove the extensionally equality of two streams :g:`s1` and :g:`s2`
 we have to construct an infinite proof of equality, that is, an infinite object
 of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite objects in
-Section :ref:`CoFixpoint`.
+Section :ref:`cofixpoint`.
 
 Definition of recursive functions
 ---------------------------------
@@ -1016,12 +1029,14 @@ Definition of functions by recursion over inductive objects
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 This section describes the primitive form of definition by recursion over
-inductive objects. See Section :ref:`Function` for more advanced constructions.
-The command:
+inductive objects. See the :cmd:`Function` command for more advanced
+constructions.
+
+.. _Fixpoint:
 
 .. cmd:: Fixpoint @ident @params {struct @ident} : @type := @term.
 
-allows defining functions by pattern-matching over inductive objects
+This command allows defining functions by pattern-matching over inductive objects
 using a fixed point construction. The meaning of this declaration is to
 define :token:`ident` a recursive function with arguments specified by the
 binders in :token:`params` such that :token:`ident` applied to arguments corresponding
@@ -1063,7 +1078,8 @@ respective values to be returned, as functions of the parameters of the
 corresponding constructor. Thus here when :g:`n` equals :g:`O` we return
 :g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`.
 
-The match operator is formally described in detail in Section :ref:`Caseexpr`.
+The match operator is formally described in detail in Section
+:ref:`match-construction`.
 The system recognizes that in the inductive call :g:`(add p m)` the first
 argument actually decreases because it is a *pattern variable* coming from
 :g:`match n with`.
@@ -1151,7 +1167,10 @@ The size of trees and forests can be defined the following way:
    end.
 
 A generic command Scheme is useful to build automatically various mutual
-induction principles. It is described in Section :ref:`Scheme`.
+induction principles. It is described in Section
+:ref:`proofschemes-induction-principles`.
+
+.. _cofixpoint:
 
 Definitions of recursive objects in co-inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1160,8 +1179,8 @@ Definitions of recursive objects in co-inductive types
 
 introduces a method for constructing an infinite object of a coinductive
 type. For example, the stream containing all natural numbers can be
-introduced applying the following method to the number :ref:`O` (see
-Section :ref:`CoInductiveTypes` for the definition of :g:`Stream`, :g:`hd` and
+introduced applying the following method to the number :g:`O` (see
+Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` and
 :g:`tl`):
 
 .. coqtop:: all
@@ -1204,8 +1223,8 @@ the normal forms of a term:
 
 .. cmdv:: CoFixpoint @ident : @type := @term {+ with @ident : @type := @term }
 
-   As in the ``Fixpoint`` command (see Section :ref:`Fixpoint`), it is possible
-   to introduce a block of mutually dependent methods.
+   As in the :cmd:`Fixpoint` command, it is possible to introduce a block of
+   mutually dependent methods.
 
 .. _Assertions:
 
@@ -1214,7 +1233,7 @@ Assertions and proofs
 
 An assertion states a proposition (or a type) of which the proof (or an
 inhabitant of the type) is interactively built using tactics. The interactive
-proof mode is described in Chapter :ref:`Proof-handling` and the tactics in
+proof mode is described in Chapter :ref:`proofhandling` and the tactics in
 Chapter :ref:`Tactics`. The basic assertion command is:
 
 .. cmd:: Theorem @ident : @type.
@@ -1245,15 +1264,14 @@ the theorem is bound to the name :token:`ident` in the environment.
 
 .. cmdv:: Theorem @ident : @type {* with @ident : @type}.
 
-   This command is useful for theorems that are proved by simultaneous
-   induction over a mutually inductive assumption, or that assert
-   mutually dependent statements in some mutual co-inductive type. It is
-   equivalent to ``Fixpoint`` or ``CoFixpoint`` (see
-   Section :ref:`CoFixpoint`) but using tactics to build
-   the proof of the statements (or the body of the specification,
-   depending on the point of view). The inductive or co-inductive types
-   on which the induction or coinduction has to be done is assumed to be
-   non ambiguous and is guessed by the system.
+   This command is useful for theorems that are proved by simultaneous induction
+   over a mutually inductive assumption, or that assert mutually dependent
+   statements in some mutual co-inductive type. It is equivalent to
+   :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of
+   the statements (or the body of the specification, depending on the point of
+   view). The inductive or co-inductive types on which the induction or
+   coinduction has to be done is assumed to be non ambiguous and is guessed by
+   the system.
 
    Like in a ``Fixpoint`` or ``CoFixpoint`` definition, the induction hypotheses
    have to be used on *structurally smaller* arguments (for a ``Fixpoint``) or
@@ -1261,7 +1279,7 @@ the theorem is bound to the name :token:`ident` in the environment.
    recursive proof 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 Section :ref:`Guarded`).
+   command :cmd:`Guarded`.
 
    The command can be used also with ``Lemma``, ``Remark``, etc. instead of
    ``Theorem``.
@@ -1270,12 +1288,12 @@ the theorem is bound to the name :token:`ident` in the environment.
 
    This allows defining a term of type :token:`type` using the proof editing
    mode. It behaves as Theorem but is intended to be used in conjunction with
-   Defined (see :ref:`Defined`) in order to define a constant of which the
-   computational behavior is relevant.
+   :cmd:`Defined` in order to define a constant of which the computational
+   behavior is relevant.
 
-   The command can be used also with ``Example`` instead of ``Definition``.
+   The command can be used also with :cmd:`Example` instead of :cmd:`Definition`.
 
-   See also Sections :ref:`Opaque` :ref:`Transparent` :ref:`unfold`.
+   See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
 .. cmdv:: Let @ident : @type.
 
@@ -1301,7 +1319,7 @@ A proof starts by the keyword Proof. Then Coq enters the proof editing mode
 until the proof is completed. The proof editing mode essentially contains
 tactics that are described in chapter :ref:`Tactics`. Besides tactics, there are
 commands to manage the proof editing mode. They are described in Chapter
-:ref:`Proof-handling`. When the proof is completed it should be validated and
+:ref:`proofhandling`. When the proof is completed it should be validated and
 put in the environment using the keyword Qed.
 
 .. exn:: @ident already exists
@@ -1319,7 +1337,7 @@ put in the environment using the keyword Qed.
       side, Qed (or Defined, see below) is mandatory to validate a proof.
 
    #. Proofs ended by Qed are declared opaque. Their content cannot be
-      unfolded (see :ref:`Conversion-tactics`), thus
+      unfolded (see :ref:`performingcomputations`), thus
       realizing some form of *proof-irrelevance*. To be able to unfold a
       proof, the proof should be ended by Defined (see below).
 
@@ -1328,7 +1346,7 @@ put in the environment using the keyword Qed.
    Same as ``Proof. … Qed.`` but the proof is then declared transparent,
    which means that its content can be explicitly used for
    type-checking and that it can be unfolded in conversion tactics
-   (see :ref:`Conversion-tactics,Opaque,Transparent`).
+   (see :ref:`performingcomputations`, :cmd:`Opaque`, :cmd:`Transparent`).
 
 .. cmdv:: Proof. … Admitted.