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).

1 files changed, 8 insertions, 9 deletions

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
 +++++++++++++++++