[Manual] Improve chapter Type classes, and add mention of Context under Variable

- More consistent code indentation
- Nest command variants properly
- Make `Context` explanation a bit less terse, with more links
- Typesetting bits, add some :cmd: links

2 files changed, 84 insertions, 65 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index c7ea7e326f..a463a73bef 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -15,24 +15,25 @@ Class and Instance declarations
 The syntax for class and instance declarations is the same as the record
 syntax of Coq:
 
-``Class Id (`` |p_1| ``:`` |t_1| ``) ⋯ (`` |p_n| ``:`` |t_n| ``) [:
-sort] := {`` |f_1| ``:`` |u_1| ``; ⋮`` |f_m| ``:`` |u_m| ``}.``
+.. coqdoc::
 
-``Instance ident : Id`` |p_1| ``⋯`` |p_n| ``:= {`` |f_1| ``:=`` |t_1| ``; ⋮`` |f_m| ``:=`` |t_m| ``}.``
+  Class classname (p1 : t1) ⋯ (pn : tn) [: sort] := { f1 : u1 ; ⋯ ; fm : um }.
 
-The |p_i| ``:`` |t_i| variables are called the *parameters* of the class and
-the |f_i| ``:`` |t_i| are called the *methods*. Each class definition gives
+  Instance instancename q1 ⋯ qm : classname p1 ⋯ pn := { f1 := t1 ; ⋯ ; fm := tm }.
+
+The ``pi : ti`` variables are called the *parameters* of the class and
+the ``fi : ti`` are called the *methods*. Each class definition gives
 rise to a corresponding record declaration and each instance is a
-regular definition whose name is given by ident and type is an
+regular definition whose name is given by `instancename` and type is an
 instantiation of the record type.
 
 We’ll use the following example class in the rest of the chapter:
 
 .. coqtop:: in
 
-   Class EqDec (A : Type) := {
-     eqb : A -> A -> bool ;
-     eqb_leibniz : forall x y, eqb x y = true -> x = y }.
+   Class EqDec (A : Type) :=
+     { eqb : A -> A -> bool ;
+       eqb_leibniz : forall x y, eqb x y = true -> x = y }.
 
 This class implements a boolean equality test which is compatible with
 Leibniz equality on some type. An example implementation is:
@@ -40,9 +41,11 @@ Leibniz equality on some type. An example implementation is:
 .. coqtop:: in
 
    Instance unit_EqDec : EqDec unit :=
-    { eqb x y := true ;
-      eqb_leibniz x y H :=
-            match x, y return x = y with tt, tt => eq_refl tt end }.
+     { eqb x y := true ;
+       eqb_leibniz x y H :=
+         match x, y return x = y with
+         | tt, tt => eq_refl tt
+         end }.
 
 Using :cmd:`Program Instance`, if one does not give all the members in
 the Instance declaration, Coq generates obligations for the remaining
@@ -52,7 +55,7 @@ fields, e.g.:
 
    Require Import Program.Tactics.
    Program Instance eq_bool : EqDec bool :=
-   { eqb x y := if x then y else negb y }.
+     { eqb x y := if x then y else negb y }.
 
 .. coqtop:: all
 
@@ -127,9 +130,9 @@ the constraints as a binding context before the instance, e.g.:
 .. coqtop:: in
 
    Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
-   { eqb x y := match x, y with
-                | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
-                end }.
+     { eqb x y := match x, y with
+                  | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
+                  end }.
 
 .. coqtop:: none
 
@@ -138,6 +141,8 @@ the constraints as a binding context before the instance, e.g.:
 These instances are used just as well as lemmas in the instance hint
 database.
 
+.. _contexts:
+
 Sections and contexts
 ---------------------
 
@@ -150,9 +155,9 @@ vernacular, except it accepts any binding context as argument. For example:
 
    Section EqDec_defs.
 
-     Context `{EA : EqDec A}.
+   Context `{EA : EqDec A}.
 
-     Global Program Instance option_eqb : EqDec (option A) :=
+   Global Program Instance option_eqb : EqDec (option A) :=
      { eqb x y := match x, y with
             | Some x, Some y => eqb x y
             | None, None => true
@@ -164,7 +169,7 @@ vernacular, except it accepts any binding context as argument. For example:
 
    About option_eqb.
 
-Here the Global modifier redeclares the instance at the end of the
+Here the :cmd:`Global` modifier redeclares the instance at the end of the
 section, once it has been generalized by the context variables it
 uses.
 
@@ -188,7 +193,7 @@ superclasses as a binding context:
 Contrary to Haskell, we have no special syntax for superclasses, but
 this declaration is equivalent to:
 
-::
+.. coqdoc::
 
     Class `(E : EqDec A) => Ord A :=
       { le : A -> A -> bool }.
@@ -248,8 +253,8 @@ explanation). These may be used as parts of other classes:
 .. coqtop:: all
 
    Class PreOrder (A : Type) (R : relation A) :=
-   { PreOrder_Reflexive :> Reflexive A R ;
-     PreOrder_Transitive :> Transitive A R }.
+     { PreOrder_Reflexive :> Reflexive A R ;
+       PreOrder_Transitive :> Transitive A R }.
 
 The syntax ``:>`` indicates that each ``PreOrder`` can be seen as a
 ``Reflexive`` relation. So each time a reflexive relation is needed, a
@@ -275,31 +280,29 @@ Summary of the commands
    The :cmd:`Class` command is used to declare a typeclass with parameters
    ``binders`` and fields the declared record fields.
 
-Variants:
+   .. _singleton-class:
 
-.. _singleton-class:
+   .. cmdv:: Class @ident {? @binders} : {? @sort} := @ident : @term
 
-.. cmd:: Class @ident {? @binders} : {? @sort} := @ident : @term
+      This variant declares a *singleton* class with a single method.  This
+      singleton class is a so-called definitional class, represented simply
+      as a definition ``ident binders := term`` and whose instances are
+      themselves objects of this type. Definitional classes are not wrapped
+      inside records, and the trivial projection of an instance of such a
+      class is convertible to the instance itself. This can be useful to
+      make instances of existing objects easily and to reduce proof size by
+      not inserting useless projections. The class constant itself is
+      declared rigid during resolution so that the class abstraction is
+      maintained.
 
-   This variant declares a *singleton* class with a single method.  This
-   singleton class is a so-called definitional class, represented simply
-   as a definition ``ident binders := term`` and whose instances are
-   themselves objects of this type. Definitional classes are not wrapped
-   inside records, and the trivial projection of an instance of such a
-   class is convertible to the instance itself. This can be useful to
-   make instances of existing objects easily and to reduce proof size by
-   not inserting useless projections. The class constant itself is
-   declared rigid during resolution so that the class abstraction is
-   maintained.
+   .. cmdv:: Existing Class @ident
 
-.. cmd:: Existing Class @ident
+      This variant declares a class a posteriori from a constant or
+      inductive definition. No methods or instances are defined.
 
-   This variant declares a class a posteriori from a constant or
-   inductive definition. No methods or instances are defined.
+      .. warn:: @ident is already declared as a typeclass
 
-   .. warn:: @ident is already declared as a typeclass
-
-      This command has no effect when used on a typeclass.
+         This command has no effect when used on a typeclass.
 
 .. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
 
@@ -314,32 +317,33 @@ Variants:
    :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 @term__1 … @term__n [| 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 :n:`forall @binders, @class
-   @term__1 … @term__n`.  One need not even mention the unique field name for
-   singleton classes.
+      This syntax is used for declaration of singleton class instances or
+      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
+   .. cmdv:: Global Instance
+      :name: Global Instance
 
-   One can use the ``Global`` modifier on instances declared in a
-   section so that their generalization is automatically redeclared
-   after the section is closed.
+      One can use the :cmd:`Global` modifier on instances declared in a
+      section so that their generalization is automatically redeclared
+      after the section is closed.
 
-.. cmdv:: Program Instance
-   :name: Program Instance
+   .. cmdv:: Program Instance
+      :name: Program Instance
 
-   Switches the type checking to Program (chapter :ref:`programs`) and
-   uses the obligation mechanism to manage missing fields.
+      Switches the type checking to `Program` (chapter :ref:`programs`) and
+      uses the obligation mechanism to manage missing fields.
 
-.. cmdv:: Declare Instance
-   :name: Declare Instance
+   .. cmdv:: Declare Instance
+      :name: Declare Instance
 
-   In a Module Type, this command states that a corresponding concrete
-   instance should exist in any implementation of this Module Type. This
-   is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or
-   between :cmd:`Declare Module` and :cmd:`Module`.
+      In a :cmd:`Module Type`, this command states that a corresponding concrete
+      instance should exist in any implementation of this :cmd:`Module Type`. This
+      is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or
+      between :cmd:`Declare Module` and :cmd:`Module`.
 
 
 Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
@@ -356,8 +360,21 @@ few other commands related to typeclasses.
 
 .. cmd:: Context @binders
 
-   Declares variables according to the given binding context, which might
-   use :ref:`implicit-generalization`.
+   Declare variables in the context of the current section, like :cmd:`Variable`,
+   but also allowing implicit variables and :ref:`implicit-generalization`.
+
+   .. coqdoc::
+
+       Section ContextExample.
+
+       Context {A : Type} (a b : A).
+       Context `{EqDec A}.
+
+       (* ... *)
+
+       End ContextExample.
+
+   See also :ref:`contexts`.
 
 .. tacn:: typeclasses eauto
    :name: typeclasses eauto
@@ -449,9 +466,8 @@ By default, all constants and local variables are considered transparent. One
 should take care not to make opaque any constant that is used to abbreviate a
 type, like:
 
-::
-
-   relation A := A -> A -> Prop.
+.. coqdoc::
+   Definition relation A := A -> A -> Prop.
 
 This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 02fb9d84ce..158a3f5ffc 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -639,6 +639,9 @@ has type :token:`type`.
    parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out
    of any section is equivalent to using :cmd:`Local Parameter`.
 
+   See also :cmd:`Context`, a variant of :cmd:`Variable` where variables can be
+   made implicit and allowing :ref:`implicit-generalization`.
+
    .. exn:: @ident already exists.
       :name: @ident already exists. (Variable)
       :undocumented: