Document Variant properly.

Cf. Enrico's remark at https://github.com/coq/coq/pull/7536#issuecomment-389826121

This commit also marginally improves the Record doc (a lot more remains to do).

2 files changed, 24 insertions, 31 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 96e33cc26..6ea1c162f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -13,42 +13,37 @@ Extensions of |Gallina|
 Record types
 ----------------
 
-The ``Record`` construction is a macro allowing the definition of
+The :cmd:`Record` construction is a macro allowing the definition of
 records as is done in many programming languages. Its syntax is
-described in the grammar below. In fact, the ``Record`` macro is more general
+described in the grammar below. In fact, the :cmd:`Record` macro is more general
 than the usual record types, since it allows also for “manifest”
-expressions. In this sense, the ``Record`` construction allows defining
+expressions. In this sense, the :cmd:`Record` construction allows defining
 “signatures”.
 
 .. _record_grammar:
 
   .. productionlist:: `sentence`
-     record         : `record_keyword` ident [binders] [: sort] := [ident] { [`field` ; … ; `field`] }.
+     record         : `record_keyword` `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }.
      record_keyword : Record | Inductive | CoInductive
-     field          : name [binders] : type [ where notation ]
-                    : | name [binders] [: term] := term
+     field          : `ident` [ `binders` ] : `type` [ where `notation` ]
+                    : | `ident` [ `binders` ] [: `type` ] := `term`
 
 In the expression:
 
-.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } }
+.. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } }
 
-the first identifier `ident` is the name of the defined record and `sort` is its
+the first identifier :token:`ident` is the name of the defined record and :token:`sort` is its
 type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted,
-the default name ``Build_``\ `ident`, where `ident` is the record name, is used. If `sort` is
+the default name ``Build_``\ :token:`ident`, where :token:`ident` is the record name, is used. If :token:`sort` is
 omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of
-fields. For a given field `ident`, its type is :g:`forall binder …, term`.
+fields. For a given field :token:`ident`, its type is :g:`forall binders, type`.
 Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the
-order of the fields is important. Finally, each `param` is a parameter of the record.
+order of the fields is important. Finally, :token:`binders` are parameters of the record.
 
 More generally, a record may have explicitly defined (a.k.a. manifest)
 fields. For instance, we might have:
-
-.. coqtop:: in
-
-  Record ident param : sort := { ident₁ : type₁ ; ident₂ := term₂ ; ident₃ : type₃ }.
-
-in which case the correctness of |type_3| may rely on the instance |term_2| of |ident_2| and |term_2| in turn
-may depend on |ident_1|.
+:n:`Record @ident @binders : @sort := { @ident₁ : @type₁ ; @ident₂ := @term₂ ; @ident₃ : @type₃ }`.
+in which case the correctness of :n:`@type₃` may rely on the instance :n:`@term₂` of :n:`@ident₂` and :n:`@term₂` may in turn depend on :n:`@ident₁`.
 
 .. example::
 
@@ -69,11 +64,10 @@ depends on both ``top`` and ``bottom``.
 
 Let us now see the work done by the ``Record`` macro. First the macro
 generates a variant type definition with just one constructor:
+:n:`Variant @ident {? @binders } : @sort := @ident₀ {? @binders }`.
 
-.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)}
-
-To build an object of type `ident`, one should provide the constructor
-|ident_0| with the appropriate number of terms filling the fields of the record.
+To build an object of type :n:`@ident`, one should provide the constructor
+:n:`@ident₀` with the appropriate number of terms filling the fields of the record.
 
 .. example:: Let us define the rational :math:`1/2`:
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index aa96f00a0..c4987a8f7 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -871,18 +871,17 @@ Parametrized inductive types
          Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
 
 Variants
-++++++++
+~~~~~~~~
 
-.. coqtop:: in
-
-   Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B.
+.. cmd:: Variant @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type}
 
-The ``Variant`` keyword is identical to the ``Inductive`` keyword, except
-that it disallows recursive definition of types (in particular lists cannot
-be defined with the Variant keyword). No induction scheme is generated for
-this variant, unless :opt:`Nonrecursive Elimination Schemes` is set.
+   The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except
+   that it disallows recursive definition of types (for instance, lists cannot
+   be defined using :cmd:`Variant`). No induction scheme is generated for
+   this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on.
 
-.. exn:: The @num th argument of @ident must be @ident in @type.
+   .. exn:: The @num th argument of @ident must be @ident in @type.
+      :undocumented:
 
 New from Coq V8.1
 +++++++++++++++++