Merge PR #7252: Sphinx doc fix warnings

2 files changed, 36 insertions, 31 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 583b73e53d..8a24a382a5 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -3,6 +3,8 @@
 Proof schemes
 ===============
 
+.. _proofschemes-induction-principles:
+
 Generation of induction principles with ``Scheme``
 --------------------------------------------------------
 
@@ -106,11 +108,10 @@ induction principles when defining a new inductive type with the
 ``Unset Elimination Schemes`` command. It may be reactivated at any time with
 ``Set Elimination Schemes``.
 
-The types declared with the keywords ``Variant`` (see :ref:`TODO-1.3.3`) and ``Record``
-(see :ref:`Record Types <record-types>`) do not have an automatic declaration of the induction
-principles. It can be activated with the command
-``Set Nonrecursive Elimination Schemes``. It can be deactivated again with
-``Unset Nonrecursive Elimination Schemes``.
+.. opt:: Nonrecursive Elimination Schemes
+
+This option controls whether types declared with the keywords :cmd:`Variant` and
+:cmd:`Record` get an automatic declaration of the induction principles.
 
 In addition, the ``Case Analysis Schemes`` flag governs the generation of
 case analysis lemmas for inductive types, i.e. corresponding to the
@@ -163,6 +164,8 @@ concluded by the conjunction of their conclusions.
 
     Check tree_forest_mutind.
 
+.. _functional-scheme:
+
 Generation of induction principles with ``Functional`` ``Scheme``
 -----------------------------------------------------------------
 
@@ -229,7 +232,7 @@ definition written by the user.
     simpl; auto with arith.
     Qed.
 
-  We can use directly the functional induction (:ref:`TODO-8.5.5`) tactic instead
+  We can use directly the functional induction (:tacn:`function induction`) tactic instead
   of the pattern/apply trick:
 
   .. coqtop:: all
@@ -305,6 +308,8 @@ definition written by the user.
   .. coqtop:: all
 
     Check tree_size_ind2.
+
+.. _derive-inversion:
      
 Generation of inversion principles with ``Derive`` ``Inversion``
 -----------------------------------------------------------------
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 531295b63a..9965d5002d 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -345,13 +345,13 @@ inductive type or a recursive constant and a notation for it.
 Simultaneous definition of terms and notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Thanks to reserved notations, the inductive, co-inductive, record, recursive
-and corecursive definitions can benefit of customized notations. To do
-this, insert a ``where`` notation clause after the definition of the
-(co)inductive type or (co)recursive term (or after the definition of
-each of them in case of mutual definitions). The exact syntax is given
-on Figure 12.1 for inductive, co-inductive, recursive and corecursive
-definitions and on Figure :ref:`record-syntax` for records. Here are examples:
+Thanks to reserved notations, the inductive, co-inductive, record, recursive and
+corecursive definitions can benefit of customized notations. To do this, insert
+a ``where`` notation clause after the definition of the (co)inductive type or
+(co)recursive term (or after the definition of each of them in case of mutual
+definitions). The exact syntax is given by :token:`decl_notation` for inductive,
+co-inductive, recursive and corecursive definitions and in :ref:`record-types`
+for records. Here are examples:
 
 .. coqtop:: in
 
@@ -381,23 +381,21 @@ Displaying informations about notations
    :opt:`Printing All`
       To disable other elements in addition to notations.
 
+.. _locating-notations:
+
 Locating notations
 ~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Locate @symbol
-
-   To know to which notations a given symbol belongs to, use the command
-   ``Locate symbol``, where symbol is any (composite) symbol surrounded by double
-   quotes. To locate a particular notation, use a string where the variables of the
-   notation are replaced by “_” and where possible single quotes inserted around
-   identifiers or tokens starting with a single quote are dropped.
-
-   .. coqtop:: all
+To know to which notations a given symbol belongs to, use the :cmd:`Locate`
+command. You can call it on any (composite) symbol surrounded by double quotes.
+To locate a particular notation, use a string where the variables of the
+notation are replaced by “_” and where possible single quotes inserted around
+identifiers or tokens starting with a single quote are dropped.
 
-      Locate "exists".
-      Locate "exists _ .. _ , _".
+.. coqtop:: all
 
-   .. todo:: See also: Section 6.3.10.
+   Locate "exists".
+   Locate "exists _ .. _ , _".
 
 Notations and binders
 ~~~~~~~~~~~~~~~~~~~~~
@@ -435,8 +433,7 @@ Binders bound in the notation and parsed as patterns
 
 In the same way as patterns can be used as binders, as in
 :g:`fun '(x,y) => x+y` or :g:`fun '(existT _ x _) => x`, notations can be
-defined so that any pattern (in the sense of the entry :n:`@pattern` of
-Figure :ref:`term-syntax-aux`) can be used in place of the
+defined so that any :n:`@pattern` can be used in place of the
 binder. Here is an example:
 
 .. coqtop:: in reset
@@ -475,7 +472,7 @@ variable. Here is an example showing the difference:
 
 The default level for a ``pattern`` is 0. One can use a different level by
 using ``pattern at level`` :math:`n` where the scale is the same as the one for
-terms (Figure :ref:`init-notations`).
+terms (see :ref:`init-notations`).
 
 Binders bound in the notation and parsed as terms
 +++++++++++++++++++++++++++++++++++++++++++++++++
@@ -491,7 +488,7 @@ the following:
 
 This is so because the grammar also contains rules starting with :g:`{}` and
 followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the
-constant :g:`sumbool` (see Section :ref:`sumbool`).
+constant :g:`sumbool` (see Section :ref:`specification`).
 
 Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning
 that ``x`` is parsed as a term at level 99 (as done in the notation for
@@ -829,6 +826,8 @@ lonely notations. These scopes, in opening order, are ``core_scope``,
    These variants survive sections. They behave as if Global were absent when
    not inside a section.
 
+.. _LocalInterpretationRulesForNotations:
+
 Local interpretation rules for notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -859,6 +858,7 @@ Binding arguments of a constant to an interpretation scope
 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
 .. cmd:: Arguments @qualid {+ @name%@scope}
+   :name: Arguments (scopes)
 
    It is possible to set in advance that some arguments of a given constant have
    to be interpreted in a given scope. The command is
@@ -897,7 +897,7 @@ Binding arguments of a constant to an interpretation scope
 .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes
 
    Defines extra argument scopes, to be used in case of coercion to Funclass
-   (see Chapter :ref:`Coercions-full`) or with a computed type.
+   (see Chapter :ref:`implicitcoercions`) or with a computed type.
 
 .. cmdv:: Global Arguments @qualid {+ @name%@scope}
 
@@ -957,7 +957,7 @@ Binding types of arguments to an interpretation scope
    type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted
    in scope ``scope``.
 
-   More generally, any coercion :n:`@class` (see Chapter :ref:`Coercions-full`)
+   More generally, any coercion :n:`@class` (see Chapter :ref:`implicitcoercions`)
    can be bound to an interpretation scope. The command to do it is
    :n:`Bind Scope @scope with @class`