Merge PR #7252: Sphinx doc fix warnings

4 files changed, 216 insertions, 166 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 13d20d7cf1..5a2aa0a1f8 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:
@@ -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
@@ -709,8 +721,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::
@@ -825,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.
 
@@ -836,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.
 
@@ -846,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:
 
@@ -891,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`
@@ -942,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.
 
@@ -1014,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.
@@ -1058,7 +1074,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 +1104,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 +1127,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::
@@ -1219,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
@@ -1278,7 +1296,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`.
@@ -1625,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
@@ -1684,7 +1701,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 82ced65b4a..6af6e78972 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
@@ -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
 ~~~~~~~~~
@@ -90,6 +91,8 @@ Notation          Precedence    Associativity
 ``_ ^ _``         30            right
 ================  ============  ===============
 
+.. _coq-library-logic:
+
 Logic
 ~~~~~
 
@@ -521,7 +524,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 +756,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.
@@ -927,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 6877759806..f474eade71 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``.
 
@@ -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:`TODO-4.5.3-case-expr`).
+     `ident` (see :cmd:`Fixpoint` and :ref:`Destructors`).
   #. The type of the projections `ident` depends on previous
      projections which themselves could not be defined.
 
@@ -212,9 +212,9 @@ 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:`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:
 
@@ -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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -626,7 +627,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 +640,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 +712,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.
@@ -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.
@@ -771,13 +772,14 @@ 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
 -----------------
 
 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.
@@ -847,7 +849,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 +935,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 +1195,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
@@ -1241,13 +1241,11 @@ 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
 ---------------------------------
 
+.. _names-of-libraries:
+
 Names of libraries
 ~~~~~~~~~~~~~~~~~~
 
@@ -1255,15 +1253,16 @@ 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
 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,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:`TODO-6.5.1-Require`), Import and Export (see :ref:`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
@@ -1326,16 +1325,15 @@ 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:
 
 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 +1369,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 +1377,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 +1385,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
 ------------------
@@ -1586,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
@@ -1799,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
 ~~~~~~~~~~~~~~~~~~~~~
 
@@ -2098,6 +2100,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,21 +2139,24 @@ 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
-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:`TODO-4.1.1-sorts`) can be printed using the command
+(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
@@ -2158,12 +2164,13 @@ 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
 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.
@@ -2220,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:
 
@@ -2245,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
 
@@ -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 2a146c57aa..246f45b3e7 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
@@ -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`
@@ -186,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
 --------------------------------------------
 
@@ -201,9 +205,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::
 
@@ -228,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
 -------
 
@@ -310,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
 ---------
@@ -328,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
 ------------------
 
@@ -348,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
@@ -415,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
@@ -458,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` :
@@ -484,6 +491,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
 ==============
 
@@ -527,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
 -----------
 
@@ -538,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
@@ -564,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
 
@@ -576,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
 
@@ -605,6 +617,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-definitions:
+
 Definitions
 -----------
 
@@ -614,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
@@ -622,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.
 
@@ -648,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.
@@ -661,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.
 
@@ -681,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
 ---------------------
@@ -701,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
@@ -842,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
 
@@ -885,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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -954,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
 ~~~~~~~~~~~~~~~~~~
@@ -976,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
 
@@ -1001,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
 ---------------------------------
@@ -1010,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
@@ -1057,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`.
@@ -1145,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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1154,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
@@ -1198,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:
 
@@ -1208,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.
@@ -1239,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
@@ -1255,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``.
@@ -1264,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.
 
@@ -1295,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
@@ -1313,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).
 
@@ -1322,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.