Convert Vernacular section of gallina chapter to use prodn

Makefile.doc

@@ -247,7 +247,7 @@ PLUGIN_MLGS := $(wildcard plugins/*/*.mlg)
 OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg
 DOC_MLGS := */*.mlg $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS)))
 DOC_EDIT_MLGS := doc/tools/docgram/*.edit_mlg
-DOC_RSTS := doc/sphinx/*.rst doc/sphinx/*/*.rst
+DOC_RSTS := doc/sphinx/*/*.rst
 
 doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
 	$(SHOW)'DOC_GRAM'
@@ -256,7 +256,7 @@ doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS)
 #todo: add a dependency of sphinx on updated_rsts when we're ready
 doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: $(DOC_GRAM) $(DOC_EDIT_MLGS)
 	$(SHOW)'DOC_GRAM_RSTS'
-	$(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS)
+	$(HIDE)$(DOC_GRAM) -check-cmds $(DOC_MLGS) $(DOC_RSTS)
 
 doc/tools/docgram/updated_rsts: doc/tools/docgram/orderedGrammar
 

doc/sphinx/README.rst

@@ -34,14 +34,14 @@ Names (link targets) are auto-generated for most simple objects, though they can
 
 Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the ``:undocumented:`` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
 
-   .. cmdv:: Lemma @ident {? @binders} : @type
-             Remark @ident {? @binders} : @type
-             Fact @ident {? @binders} : @type
-             Corollary @ident {? @binders} : @type
-             Proposition @ident {? @binders} : @type
+   .. cmdv:: Lemma @ident {* @binder } : @type
+             Remark @ident {* @binder } : @type
+             Fact @ident {* @binder } : @type
+             Corollary @ident {* @binder } : @type
+             Proposition @ident {* @binder } : @type
       :name: Lemma; Remark; Fact; Corollary; Proposition
 
-      These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.
+      These commands are all synonyms of :n:`Theorem @ident {* @binder } : type`.
 
 Notations
 ---------
@@ -89,10 +89,15 @@ Objects
 
 Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL):
 
+``.. attr::`` :black_nib: An attribute.
+    Example::
+
+       .. attr:: local
+
 ``.. cmd::`` :black_nib: A Coq command.
     Example::
 
-       .. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+       .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident }
 
           This command is equivalent to :n:`…`.
 

doc/sphinx/README.template.rst

@@ -34,14 +34,14 @@ Names (link targets) are auto-generated for most simple objects, though they can
 
 Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the ``:undocumented:`` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
 
-   .. cmdv:: Lemma @ident {? @binders} : @type
-             Remark @ident {? @binders} : @type
-             Fact @ident {? @binders} : @type
-             Corollary @ident {? @binders} : @type
-             Proposition @ident {? @binders} : @type
+   .. cmdv:: Lemma @ident {* @binder } : @type
+             Remark @ident {* @binder } : @type
+             Fact @ident {* @binder } : @type
+             Corollary @ident {* @binder } : @type
+             Proposition @ident {* @binder } : @type
       :name: Lemma; Remark; Fact; Corollary; Proposition
 
-      These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`.
+      These commands are all synonyms of :n:`Theorem @ident {* @binder } : type`.
 
 Notations
 ---------

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

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

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:
 

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.
 

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

doc/sphinx/conf.py

@@ -183,16 +183,21 @@ def setup(app):
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
+    'binders',
     'collection',
     'command',
+    'definition',
     'dirpath',
+    'inductive',
+    'ind_body',
     'modpath',
     'module',
-    'red_expr',
+    'simple_tactic',
     'symbol',
     'tactic',
     'term_pattern',
     'term_pattern_string',
+    'toplevel_selector',
 ]]
 
 # -- Options for HTML output ----------------------------------------------

doc/sphinx/coq-cmdindex.rst

@@ -2,6 +2,8 @@
 
 .. hack to get index in TOC
 
+.. _command_index:
+
 -----------------
 Command index
 -----------------

doc/sphinx/coq-tacindex.rst

@@ -2,6 +2,8 @@
 
 .. hack to get index in TOC
 
+.. _tactic_index:
+
 -------------
 Tactic index
 -------------