Add indexes for coercion / substructure symbol :>.

And a few more Sphinx fixes in passing.

4 files changed, 15 insertions, 10 deletions

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c8fb4bd00e..789890eab5 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -285,19 +285,21 @@ Activating the Printing of Coercions
 Classes as Records
 ------------------
 
+.. index:: :> (coercion)
+
 We allow the definition of *Structures with Inheritance* (or classes as records)
 by extending the existing :cmd:`Record` macro. Its new syntax is:
 
 .. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }
 
-   The first identifier `ident` is the name of the defined record and
-   `sort` is its type. The optional identifier after ``:=`` is the name
-   of the constuctor (it will be ``Build_``\ `ident` if not given).
-   The other identifiers are the names of the fields, and the `term`
+   The first identifier :token:`ident` is the name of the defined record and
+   :token:`sort` is its type. The optional identifier after ``:=`` is the name
+   of the constuctor (it will be :n:`Build_@ident` if not given).
+   The other identifiers are the names of the fields, and :token:`term`
    are their respective types. If ``:>`` is used instead of ``:`` in
    the declaration of a field, then the name of this field is automatically
    declared as a coercion from the record name to the class of this
-   field type. Remark that the fields always verify the uniform
+   field type. Note that the fields always verify the uniform
    inheritance condition. If the optional ``>`` is given before the
    record name, then the constructor name is automatically declared as
    a coercion from the class of the last field type to the record name
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index cc8870e2e4..e153c7cbe2 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -102,7 +102,7 @@ Syntactic control over equalities
 
 To give more control over the generation of equalities, the
 type checker will fall back directly to |Coq|’s usual typing of dependent
-pattern matching if a return or in clause is specified. Likewise, the
+pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the
 if construct is not treated specially by |Program| so boolean tests in
 the code are not automatically reflected in the obligations. One can
 use the :g:`dec` combinator to get the correct hypotheses as in:
@@ -118,8 +118,9 @@ use the :g:`dec` combinator to get the correct hypotheses as in:
      else S (pred n).
 
 The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not
-produce an equality, contrary to the let pattern construct :g:`let ’(x1,
-..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to
+produce an equality, contrary to the let pattern construct
+:g:`let '(x1,..., xn) := t in b`.
+Also, :g:`term :>` explicitly asks the system to
 coerce term to its support type. It can be useful in notations, for
 example:
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 882798205b..98dfcb2373 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -228,6 +228,8 @@ mechanism if available, as shown in the example.
 Substructures
 ~~~~~~~~~~~~~
 
+.. index:: :> (substructure)
+
 Substructures are components of a class which are instances of a class
 themselves. They often arise when using classes for logical
 properties, e.g.:
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 85474a3e98..10650af1d1 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -97,8 +97,8 @@ Logic
 The basic library of |Coq| comes with the definitions of standard
 (intuitionistic) logical connectives (they are defined as inductive
 constructions). They are equipped with an appealing syntax enriching the
-subclass `form` of the syntactic class `term`. The syntax of `form`
-is shown below:
+subclass :token:`form` of the syntactic class :token:`term`. The syntax of
+:token:`form` is shown below:
 
 .. /!\ Please keep the blanks in the lines below, experimentally they produce
    a nice last column. Or even better, find a proper way to do this!