[Sphinx] Clean-up indices

2 files changed, 32 insertions, 21 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 8a24a382a..e12e4d897 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -12,7 +12,7 @@ The ``Scheme`` command is a high-level tool for generating automatically
 (possibly mutual) induction principles for given types and sorts. Its
 syntax follows the schema:
 
-.. cmd:: Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort}
+.. cmd:: Scheme @ident := Induction for @ident Sort sort {* with @ident := Induction for @ident Sort sort}
 
 where each `ident'ᵢ` is a different inductive type identifier 
 belonging to the same package of mutual inductive definitions. This
@@ -20,17 +20,17 @@ command generates the `identᵢ`s to be mutually recursive
 definitions. Each term `identᵢ` proves a general principle of mutual
 induction for objects in type `identᵢ`.
 
-.. cmdv:: Scheme ident := Minimality for ident' Sort sort {* with ident := Minimality for ident' Sort sort}
+.. cmdv:: Scheme @ident := Minimality for @ident Sort sort {* with @ident := Minimality for @ident' Sort sort}
 
   Same as before but defines a non-dependent elimination principle more
   natural in case of inductively defined relations.
 
-.. cmdv:: Scheme Equality for ident
+.. cmdv:: Scheme Equality for @ident
 
    Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident`
    involves some other inductive types, their equality has to be defined first.
 
-.. cmdv:: Scheme Induction for ident Sort sort {* with Induction for ident Sort sort}
+.. cmdv:: Scheme Induction for @ident Sort sort {* with Induction for @ident Sort sort}
 
    If you do not provide the name of the schemes, they will be automatically computed from the
    sorts involved (works also with Minimality).
@@ -103,6 +103,8 @@ induction for objects in type `identᵢ`.
 Automatic declaration of schemes
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
+.. opt:: Elimination Schemes
+
 It is possible to deactivate the automatic declaration of the
 induction principles when defining a new inductive type with the
 ``Unset Elimination Schemes`` command. It may be reactivated at any time with
@@ -113,15 +115,22 @@ induction principles when defining a new inductive type with the
 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
-pattern-matching term alone and without fixpoint.
-You can also activate the automatic declaration of those Boolean
-equalities (see the second variant of ``Scheme``) with respectively the
-commands ``Set Boolean Equality Schemes`` and ``Set Decidable Equality
-Schemes``. However you have to be careful with this option since Coq may
-now reject well-defined inductive types because it cannot compute a
-Boolean equality for them.
+.. opt:: Case Analysis Schemes
+
+   This flag governs the generation of case analysis lemmas for inductive types,
+   i.e. corresponding to the pattern-matching term alone and without fixpoint.
+
+.. opt:: Boolean Equality Schemes
+
+.. opt:: Decidable Equality Schemes
+
+These flags control the automatic declaration of those Boolean equalities (see
+the second variant of ``Scheme``).
+
+.. warning::
+
+   You have to be careful with this option since Coq may now reject well-defined
+   inductive types because it cannot compute a Boolean equality for them.
 
 .. opt:: Rewriting Schemes
 
@@ -134,7 +143,7 @@ The ``Combined Scheme`` command is a tool for combining induction
 principles generated by the ``Scheme command``. Its syntax follows the
 schema :
 
-.. cmd:: Combined Scheme ident from {+, ident}
+.. cmd:: Combined Scheme @ident from {+, ident}
 
 where each identᵢ after the ``from`` is a different inductive principle that must
 belong to the same package of mutual inductive principle definitions.
@@ -175,7 +184,7 @@ generating automatically induction principles corresponding to
 available via ``Require Import FunInd``. Its syntax then follows the
 schema:
 
-.. cmd:: Functional Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort}
+.. cmd:: Functional Scheme @ident := Induction for ident' Sort sort {* with @ident := Induction for @ident Sort sort}
 
 where each `ident'ᵢ` is a different mutually defined function
 name (the names must be in the same order as when they were defined). This
@@ -316,7 +325,7 @@ Generation of inversion principles with ``Derive`` ``Inversion``
 
 The syntax of ``Derive`` ``Inversion`` follows the schema:
 
-.. cmd:: Derive Inversion ident with forall (x : T), I t Sort sort
+.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort
 
 This command generates an inversion principle for the `inversion … using` 
 tactic. Let `I` be an inductive predicate and `x` the variables occurring
@@ -325,17 +334,17 @@ sort `sort` corresponding to the instance `∀ (x:T), I t` with the name
 `ident` in the global environment. When applied, it is equivalent to
 having inverted the instance with the tactic `inversion`.
 
-.. cmdv:: Derive Inversion_clear ident with forall (x:T), I t Sort sort
+.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort
 
    When applied, it is equivalent to having inverted the instance with the
    tactic inversion replaced by the tactic `inversion_clear`.
 
-.. cmdv:: Derive Dependent Inversion ident with forall (x:T), I t Sort sort
+.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort sort
 
    When applied, it is equivalent to having inverted the instance with
    the tactic `dependent inversion`.
 
-.. cmdv:: Derive Dependent Inversion_clear ident with forall(x:T), I t Sort sort
+.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort sort
 
    When applied, it is equivalent to having inverted the instance
    with the tactic `dependent inversion_clear`.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 9965d5002..c4a7121ce 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -32,6 +32,8 @@ Notations
 Basic notations
 ~~~~~~~~~~~~~~~
 
+.. cmd:: Notation
+
 A *notation* is a symbolic expression denoting some term or term
 pattern.
 
@@ -1200,7 +1202,7 @@ Tactic notations allow to customize the syntax of the tactics of the
 tactic language. Tactic notations obey the following syntax:
 
 .. productionlist:: coq
-   tacn                 : [Local] Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`.
+   tacn                 : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`.
    prod_item            : `string` | `tactic_argument_type`(`ident`)
    tactic_level         : (at level `natural`)
    tactic_argument_type : ident | simple_intropattern | reference
@@ -1211,7 +1213,7 @@ tactic language. Tactic notations obey the following syntax:
                         : | tactic | tactic0 | tactic1 | tactic2 | tactic3
                         : | tactic4 | tactic5
 
-.. cmd:: {? Local} Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic.
+.. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic.
 
    A tactic notation extends the parser and pretty-printer of tactics with a new
    rule made of the list of production items. It then evaluates into the