From e367f1113738b28c42de6c87b7c9f3d0fce3f5be Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Nov 2018 19:35:22 +0100
Subject: [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.
---
 doc/sphinx/addendum/type-classes.rst | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'doc/sphinx/addendum/type-classes.rst')

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 369dae0ead..15a55d9e72 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -298,24 +298,24 @@ Variants:
 
       This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
+.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
 
-The :cmd:`Instance` command is used to declare a typeclass instance named
-``ident`` of the class :cmd:`Class` with parameters ``t1`` to ``tn`` and
-fields ``b1`` to ``bi``, where each field must be a declared field of
-the class.  Missing fields must be filled in interactive proof mode.
+   This command is used to declare a typeclass instance named
+   :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and
+   fields ``b1`` to ``bi``, where each field must be a declared field of
+   the class.  Missing fields must be filled in interactive proof mode.
 
-An arbitrary context of ``binders`` can be put after the name of the
-instance and before the colon to declare a parameterized instance. An
-optional priority can be declared, 0 being the highest priority as for
-:tacn:`auto` hints. If the priority is not specified, it defaults to the number
-of non-dependent binders of the instance.
+   An arbitrary context of :token:`binders` can be put after the name of the
+   instance and before the colon to declare a parameterized instance. An
+   optional priority can be declared, 0 being the highest priority as for
+   :tacn:`auto` hints. If the priority is not specified, it defaults to the number
+   of non-dependent binders of the instance.
 
-.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term
+.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term
 
    This syntax is used for declaration of singleton class instances or
-   for directly giving an explicit term of type ``forall binders, Class
-   t1 … tn``.  One need not even mention the unique field name for
+   for directly giving an explicit term of type :n:`forall @binders, @class
+   @term__1 … @term__n`.  One need not even mention the unique field name for
    singleton classes.
 
 .. cmdv:: Global Instance
-- 
cgit v1.2.3