[sphinx] Fix many warnings.

Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.

2 files changed, 14 insertions, 4 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 583b73e53..1f1167c59 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``
 --------------------------------------------------------
 
@@ -163,6 +165,8 @@ concluded by the conjunction of their conclusions.
 
     Check tree_forest_mutind.
 
+.. _functional-scheme:
+
 Generation of induction principles with ``Functional`` ``Scheme``
 -----------------------------------------------------------------
 
@@ -229,7 +233,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 +309,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 531295b63..0da9f2300 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -381,6 +381,8 @@ Displaying informations about notations
    :opt:`Printing All`
       To disable other elements in addition to notations.
 
+.. _locating-notations:
+
 Locating notations
 ~~~~~~~~~~~~~~~~~~
 
@@ -491,7 +493,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 +831,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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -897,7 +901,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 +961,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`