[sphinx] Progress towards closing #7602: remove most objects without a body.

Remove objects without body from most chapters.
The remaining problems are all in the SSReflect chapter.

2 files changed, 22 insertions, 23 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 8f76085d88..418922e9b3 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__1 := Induction for @ident__2 Sort sort {* with @ident__i := Induction for @ident__j Sort sort}
+.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort @sort {* with @ident__i := Induction for @ident__j Sort @sort}
 
   This command is a high-level tool for generating automatically
   (possibly mutual) induction principles for given types and sorts.
@@ -22,10 +22,10 @@ syntax follows the schema:
   definitions. Each term :n:`@ident__i` proves a general principle of mutual
   induction for objects in type :n:`@ident__j`.
 
-.. 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.
+   Same as before but defines a non-dependent elimination principle more
+   natural in case of inductively defined relations.
 
 .. cmdv:: Scheme Equality for @ident
    :name: Scheme Equality
@@ -33,7 +33,7 @@ syntax follows the schema:
    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).
@@ -195,19 +195,18 @@ Combined Scheme
 Generation of induction principles with ``Functional`` ``Scheme``
 -----------------------------------------------------------------
 
-The ``Functional Scheme`` command is a high-level experimental tool for
-generating automatically induction principles corresponding to
-(possibly mutually recursive) functions. First, it must be made
-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__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' 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
-command generates the induction principle for each `identᵢ`, following
-the recursive structure and case analyses of the corresponding function
-identᵢ’.
+   This command is a high-level experimental tool for
+   generating automatically induction principles corresponding to
+   (possibly mutually recursive) functions. First, it must be made
+   available via ``Require Import FunInd``.
+   Each :n:`@ident__i` is a different mutually defined function
+   name (the names must be in the same order as when they were defined). This
+   command generates the induction principle for each :n:`@ident__i`, following
+   the recursive structure and case analyses of the corresponding function
+   :n:`@ident__i'`.
 
 .. warning::
 
@@ -349,17 +348,17 @@ Generation of inversion principles with ``Derive`` ``Inversion``
    :g:`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`.
@@ -377,8 +376,8 @@ Generation of inversion principles with ``Derive`` ``Inversion``
 
     Parameter P : nat -> nat -> Prop.
 
-  To generate the inversion lemma for the instance `(Le (S n) m)` and the
-  sort `Prop`, we do:
+  To generate the inversion lemma for the instance :g:`(Le (S n) m)` and the
+  sort :g:`Prop`, we do:
 
   .. coqtop:: all
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 2214cbfb34..65df89da6c 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -31,8 +31,8 @@ Basic notations
 
 .. cmd:: Notation
 
-A *notation* is a symbolic expression denoting some term or term
-pattern.
+   A *notation* is a symbolic expression denoting some term or term
+   pattern.
 
 A typical notation is the use of the infix symbol ``/\`` to denote the
 logical conjunction (and). Such a notation is declared by