Convert Gallina Vernac to use prodn

5 files changed, 19 insertions, 25 deletions

diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 9f5741f72a..94ab6e789c 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -170,7 +170,7 @@ compatibility constraints.
 Adding new relations and morphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd::  Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
+.. cmd::  Add Parametric Relation {* @binder } : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident
 
    This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`,
    :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`.
@@ -219,7 +219,7 @@ replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident
+.. cmd:: Add Parametric Morphism {* @binder } : (@ident {+ @term__1}) with signature @term__2 as @ident
 
    This command declares a parametric morphism :n:`@ident {+ @term__1}` of
    signature :n:`@term__2`.  The final identifier :token:`ident` gives a unique
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 19b33f0d90..b007509b2e 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -198,7 +198,7 @@ Figure :ref:`vernacular` as follows:
    \comindex{Hypothesis \mbox{\rm (and coercions)}}
 
 .. productionlist::
-   assumption : `assumption_keyword` `assums` .
+   assumption : `assumption_token` `assums` .
    assums : `simple_assums`
           : (`simple_assums`) ... (`simple_assums`)
    simple_assums : `ident` ... `ident` :[>] `term`
@@ -215,12 +215,6 @@ grammar of inductive types from Figure :ref:`vernacular` as follows:
    \comindex{Inductive \mbox{\rm (and coercions)}}
    \comindex{CoInductive \mbox{\rm (and coercions)}}
 
-.. productionlist::
-   inductive : Inductive `ind_body` with ... with `ind_body`
-             : CoInductive `ind_body` with ... with `ind_body`
-   ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ]
-   constructor : `ident` [ `binders` ] [:[>] `term` ]
-
 Especially, if the extra ``>`` is present in a constructor
 declaration, this constructor is declared as a coercion.
 
@@ -240,7 +234,7 @@ declaration, this constructor is declared as a coercion.
 
       Same as :cmd:`Identity Coercion` but locally to the current section.
 
-   .. cmdv:: SubClass @ident := @type
+   .. cmd:: SubClass @ident_decl @def_body
       :name: SubClass
 
       If :n:`@type` is a class :n:`@ident'` applied to some arguments then
@@ -251,7 +245,7 @@ declaration, this constructor is declared as a coercion.
       :n:`Definition @ident := @type.`
       :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`.
 
-   .. cmdv:: Local SubClass @ident := @type
+   .. cmdv:: Local SubClass @ident_decl @def_body
 
       Same as before but locally to the current section.
 
@@ -299,7 +293,7 @@ Classes as Records
 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 } }
+.. cmdv:: {| Record | Structure } {? >} @ident {* @binder } : @sort := {? @ident} { {+; @ident :{? >} @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
@@ -315,12 +309,6 @@ by extending the existing :cmd:`Record` macro. Its new syntax is:
    (this may fail if the uniform inheritance condition is not
    satisfied).
 
-.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }
-   :name: Structure
-
-   This is a synonym of :cmd:`Record`.
-
-
 Coercions and Sections
 ----------------------
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index a17dca1693..549249d25c 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -174,7 +174,7 @@ Program Definition
       .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ...
          :undocumented:
 
-   .. cmdv:: Program Definition @ident @binders : @type := @term
+   .. cmdv:: Program Definition @ident {* @binder } : @type := @term
 
       This is equivalent to:
 
@@ -189,7 +189,7 @@ Program Definition
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term
+.. cmd:: Program Fixpoint @ident {* @binder } {? {@order}} : @type := @term
 
    The optional order annotation follows the grammar:
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 57a2254100..af4e9051bb 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -295,14 +295,18 @@ the Existing Instance command to achieve the same effect.
 Summary of the commands
 -----------------------
 
-.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }
+.. cmd:: Class @inductive_definition {* with @inductive_definition }
 
    The :cmd:`Class` command is used to declare a typeclass with parameters
    :token:`binders` and fields the declared record fields.
 
+   This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+   :attr:`universes(template)`, :attr:`universes(notemplate)`,
+   :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes.
+
    .. _singleton-class:
 
-   .. cmdv:: Class @ident {? @binders} : {? @sort} := @ident : @term
+   .. cmdv:: Class @ident {* @binder } : {? @sort} := @ident : @term
 
       This variant declares a *singleton* class with a single method.  This
       singleton class is a so-called definitional class, represented simply
@@ -324,7 +328,7 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
+.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
 
    This command is used to declare a typeclass instance named
    :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and
@@ -337,10 +341,10 @@ Summary of the commands
    :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number
    of non-dependent binders of the instance.
 
-   .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term
+   .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term
 
       This syntax is used for declaration of singleton class instances or
-      for directly giving an explicit term of type :n:`forall @binders, @term__0
+      for directly giving an explicit term of type :n:`forall {* @binder }, @term__0
       {+ @term}`.  One need not even mention the unique field name for
       singleton classes.
 
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index f9cc25959c..c069782add 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -152,6 +152,8 @@ Many other commands support the ``Polymorphic`` flag, including:
 - :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint
   polymorphically, not at a single instance.
 
+.. _cumulative:
+
 Cumulative, NonCumulative
 -------------------------