Merge PR #11314: Convert productionlists in the Gallina chapter up to the Vernacular section to prodns

Reviewed-by: Zimmi48

7 files changed, 245 insertions, 332 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index f504678ef9..a34b2d5195 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -143,13 +143,12 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
           application of a tactic.
 
 ``.. prodn::`` A grammar production.
-    Use prodn to document individual grammar productions instead of Sphinx
+    Use ``.. prodn`` to document grammar productions instead of Sphinx
     `production lists
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
 
     prodn displays multiple productions together with alignment similar to ``.. productionlist``,
-    i.e. displayed in 3 columns, however
-    unlike ``.. productionlist``\ s, this directive accepts notation syntax.
+    however unlike ``.. productionlist``\ s, this directive accepts notation syntax.
 
     Example::
 
@@ -158,7 +157,8 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
         | second_production
 
        The first line defines "occ_switch", which must be unique in the document.  The second
-       references but doesn't define "term".  The third form is for continuing the
+       references and expands the definition of "term", whose main definition is elsewhere
+       in the document.  The third form is for continuing the
        definition of a nonterminal when it has multiple productions.  It leaves the first
        column in the output blank.
 
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
index 8612e51aa5..3dfe4db439 100644
--- a/doc/sphinx/_static/coqnotations.sty
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -67,7 +67,7 @@
 
 \newcssclass{notation-sup}{\nsup{#1}}
 \newcssclass{notation-sub}{\nsub{#1}}
-\newcssclass{notation}{\nnotation{#1}}
+\newcssclass{notation}{\nnotation{\textbf{#1}}}
 \newcssclass{repeat}{\nrepeat{#1}}
 \newcssclass{repeat-wrapper}{\nwrapper{#1}}
 \newcssclass{repeat-wrapper-with-sub}{\nwrapper{#1}}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index d654479b07..3806ba6ee6 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -10,6 +10,7 @@
 .notation {
     /* font-family: "Ubuntu Mono", "Consolas", monospace; */
     white-space: pre-wrap;
+    font-weight: bold;
 }
 
 .notation .notation-sup {
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 45b3f6f161..15f42591ce 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -192,7 +192,7 @@ Disjunctive patterns
 --------------------
 
 Multiple patterns that share the same right-hand-side can be
-factorized using the notation :n:`{+| @patterns_comma}`. For
+factorized using the notation :n:`{+| {+, @pattern } }`. For
 instance, :g:`max` can be rewritten as follows:
 
 .. coqtop:: in reset
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index cad5e4e67e..80f209fcf1 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -95,25 +95,23 @@ Logic
 The basic library of |Coq| comes with the definitions of standard
 (intuitionistic) logical connectives (they are defined as inductive
 constructions). They are equipped with an appealing syntax enriching the
-subclass :token:`form` of the syntactic class :token:`term`. The syntax of
-:token:`form` is shown below:
-
-.. /!\ Please keep the blanks in the lines below, experimentally they produce
-   a nice last column. Or even better, find a proper way to do this!
-
-.. productionlist::
-   form : True                                           (True)
-        : False                                          (False)
-        : ~ `form`                                         (not)
-        : `form` /\ `form`                                   (and)
-        : `form` \/ `form`                                   (or)
-        : `form` -> `form`                                   (primitive implication)
-        : `form` <-> `form`                                  (iff)
-        : forall `ident` : `type`, `form`                      (primitive for all)
-        : exists `ident` [: `specif`], `form`                  (ex)
-        : exists2 `ident` [: `specif`], `form` & `form`          (ex2)
-        : `term` = `term`                                    (eq)
-        : `term` = `term` :> `specif`                          (eq)
+subclass :token:`form` of the syntactic class :token:`term`. The constructs
+for :production:`form` are:
+
+============================================== =======
+True                                           True
+False                                          False
+:n:`~ @form`                                   not
+:n:`@form /\ @form`                            and
+:n:`@form \/ @form`                            or
+:n:`@form -> @form`                            primitive implication
+:n:`@form <-> @form`                           iff
+:n:`forall @ident : @type, @form`              primitive for all
+:n:`exists @ident {? @specif}, @form`          ex
+:n:`exists2 @ident {? @specif}, @form & @form` ex2
+:n:`@term = @term`                             eq
+:n:`@term = @term :> @specif`                  eq
+============================================== =======
 
 .. note::
 
@@ -281,19 +279,20 @@ In the basic library, we find in ``Datatypes.v`` the definition
 of the basic data-types of programming,
 defined as inductive constructions over the sort ``Set``. Some of
 them come with a special syntax shown below (this syntax table is common with
-the next section :ref:`specification`):
-
-.. productionlist::
-   specif :  `specif` * `specif`                           (prod)
-          : `specif` + `specif`                          (sum)
-          : `specif` + { `specif` }                      (sumor)
-          : { `specif` } + { `specif` }                  (sumbool)
-          : { `ident` : `specif` | `form` }              (sig)
-          : { `ident` : `specif` | `form` & `form` }       (sig2)
-          : { `ident` : `specif` & `specif` }             (sigT)
-          : { `ident` : `specif` & `specif` & `specif` }    (sigT2)
-  term : (`term`, `term`)                               (pair)
-
+the next section :ref:`specification`).  The constructs for :production:`specif` are:
+
+============================================= =======
+:n:`@specif * @specif`                        prod
+:n:`@specif + @specif`                        sum
+:n:`@specif + { @specif }`                    sumor
+:n:`{ @specif } + { @specif }`                sumbool
+:n:`{ @ident : @specif | @form }`             sig
+:n:`{ @ident : @specif | @form & @form }`     sig2
+:n:`{ @ident : @specif & @specif }`           sigT
+:n:`{ @ident : @specif & @specif & @specif }` sigT2
+============================================= =======
+
+The notation for pairs (elements of type prod) is: :n:`(@term, @term)`
 
 Programming
 +++++++++++
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index a8d6d2632b..78428be18f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -155,19 +155,19 @@ available:
 
 .. _record_projections_grammar:
 
-  .. insertgram term_projection term_projection
+  .. insertprodn term_projection term_projection
 
-  .. productionlist:: coq
-     term_projection : `term0` .( `qualid` `args_opt` )
-                     : `term0` .( @ `qualid` `term1_list_opt` )
+  .. prodn::
+     term_projection ::= @term0 .( @qualid {* @arg } )
+     | @term0 .( @ @qualid {* @term1 } )
 
   Syntax of Record projections
 
 The corresponding grammar rules are given in the preceding grammar. When :token:`qualid`
-denotes a projection, the syntax :n:`@term.(@qualid)` is equivalent to :n:`@qualid @term`,
-the syntax :n:`@term.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term`.
-and the syntax :n:`@term.(@@qualid {+ @term })` to :n:`@@qualid {+ @term } @term`.
-In each case, :token:`term` is the object projected and the
+denotes a projection, the syntax :n:`@term0.(@qualid)` is equivalent to :n:`@qualid @term0`,
+the syntax :n:`@term0.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term0`.
+and the syntax :n:`@term0.(@@qualid {+ @term0 })` to :n:`@@qualid {+ @term0 } @term0`.
+In each case, :token:`term0` is the object projected and the
 other arguments are the parameters of the inductive type.
 
 
@@ -1878,27 +1878,16 @@ Controlling the insertion of implicit arguments not followed by explicit argumen
 Explicit applications
 ~~~~~~~~~~~~~~~~~~~~~
 
-In presence of non-strict or contextual argument, or in presence of
+In presence of non-strict or contextual arguments, or in presence of
 partial applications, the synthesis of implicit arguments may fail, so
-one may have to give explicitly certain implicit arguments of an
-application. The syntax for this is :n:`(@ident := @term)` where :token:`ident` is the
-name of the implicit argument and term is its corresponding explicit
-term. Alternatively, one can locally deactivate the hiding of implicit
-arguments of a function by using the notation :n:`@qualid {+ @term }`.
-This syntax extension is given in the following grammar:
+one may have to explicitly give certain implicit arguments of an
+application. Use the :n:`(@ident := @term)` form of :token:`arg` to do so,
+where :token:`ident` is the name of the implicit argument and :token:`term`
+is its corresponding explicit term. Alternatively, one can deactivate
+the hiding of implicit arguments for a single function application using the
+:n:`@ @qualid {? @univ_annot } {* @term1 }` form of :token:`term10`.
 
-.. _explicit_app_grammar:
-
-  .. productionlist:: explicit_apps
-       term     : @ `qualid` `term` … `term`
-                : @ `qualid`
-                : `qualid` `argument` … `argument`
-       argument : `term`
-                : (`ident` := `term`)
-
-  Syntax for explicitly giving implicit arguments
-
-.. example:: (continued)
+.. example:: Syntax for explicitly giving implicit arguments (continued)
 
     .. coqtop:: all
 
@@ -2319,17 +2308,13 @@ Printing universes
 Existential variables
 ---------------------
 
-.. insertgram term_evar evar_binding
-
-.. productionlist:: coq
-   term_evar : ?[ `ident` ]
-             : ?[ ?`ident` ]
-             : ?`ident` `evar_bindings_opt`
-   evar_bindings_opt : @{ `evar_bindings_semi` }
-                     : `empty`
-   evar_bindings_semi : `evar_bindings_semi` ; `evar_binding`
-                      : `evar_binding`
-   evar_binding : `ident` := `term`
+.. insertprodn term_evar evar_binding
+
+.. prodn::
+   term_evar ::= ?[ @ident ]
+   | ?[ ?@ident ]
+   | ?@ident {? @%{ {+; @evar_binding } %} }
+   evar_binding ::= @ident := @term
 
 |Coq| terms can include existential variables which represents unknown
 subterms to eventually be replaced by actual subterms.
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 3cc101d06b..967b0461d0 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -16,27 +16,27 @@ In Coq, logical objects are typed to ensure their logical correctness.  The
 rules implemented by the typing algorithm are described in Chapter :ref:`calculusofinductiveconstructions`.
 
 
-About the grammars in the manual
-================================
+..  About the grammars in the manual
+    ================================
 
-Grammars are presented in Backus-Naur form (BNF). Terminal symbols are
-set in black ``typewriter font``. In addition, there are special notations for
-regular expressions.
+    Grammars are presented in Backus-Naur form (BNF). Terminal symbols are
+    set in black ``typewriter font``. In addition, there are special notations for
+    regular expressions.
 
-An expression enclosed in square brackets ``[…]`` means at most one
-occurrence of this expression (this corresponds to an optional
-component).
+    An expression enclosed in square brackets ``[…]`` means at most one
+    occurrence of this expression (this corresponds to an optional
+    component).
 
-The notation “``entry sep … sep entry``” stands for a non empty sequence
-of expressions parsed by entry and separated by the literal “``sep``” [1]_.
+    The notation “``entry sep … sep entry``” stands for a non empty sequence
+    of expressions parsed by entry and separated by the literal “``sep``” [1]_.
 
-Similarly, the notation “``entry … entry``” stands for a non empty
-sequence of expressions parsed by the “``entry``” entry, without any
-separator between.
+    Similarly, the notation “``entry … entry``” stands for a non empty
+    sequence of expressions parsed by the “``entry``” entry, without any
+    separator between.
 
-At the end, the notation “``[entry sep … sep entry]``” stands for a
-possibly empty sequence of expressions parsed by the “``entry``” entry,
-separated by the literal “``sep``”.
+    At the end, the notation “``[entry sep … sep entry]``” stands for a
+    possibly empty sequence of expressions parsed by the “``entry``” entry,
+    separated by the literal “``sep``”.
 
 .. _lexical-conventions:
 
@@ -58,10 +58,12 @@ Identifiers
   recognized by the following grammar (except that the string ``_`` is reserved;
   it is not a valid identifier):
 
-  .. productionlist:: coq
-     ident             : `first_letter`[`subsequent_letter`…`subsequent_letter`]
-     first_letter      : a..z ∣ A..Z ∣ _ ∣ `unicode_letter`
-     subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part`
+  .. insertprodn ident subsequent_letter
+
+  .. prodn::
+     ident ::= @first_letter {* @subsequent_letter }
+     first_letter ::= {| a .. z | A .. Z | _ | @unicode_letter }
+     subsequent_letter ::= {| @first_letter | @digit | ' | @unicode_id_part }
 
   All characters are meaningful. In particular, identifiers are case-sensitive.
   :production:`unicode_letter` non-exhaustively includes Latin,
@@ -77,13 +79,13 @@ Numerals
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
-  .. productionlist:: coq
-     numeral : `num`[. `num`][`exp`[`sign`]`num`]
-     int     : [-]`num`
-     num     : `digit`…`digit`
-     digit   : 0..9
-     exp     : e | E
-     sign    : + | -
+  .. insertprodn numeral digit
+
+  .. prodn::
+     numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } }
+     int ::= {? - } {+ @digit }
+     num ::= {+ @digit }
+     digit ::= 0 .. 9
 
 Strings
   Strings begin and end with ``"`` (double quote).  Use ``""`` to represent
@@ -139,50 +141,39 @@ presentation of Cic is given in Chapter :ref:`calculusofinductiveconstructions`.
 are given in Chapter :ref:`extensionsofgallina`. How to customize the syntax
 is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
 
-.. insertgram term binders_opt
-
-.. productionlist:: coq
-   term : forall `open_binders` , `term`
-        : fun `open_binders` => `term`
-        : `term_let`
-        : if `term` `as_return_type_opt` then `term` else `term`
-        : `term_fix`
-        : `term100`
-   term100 : `term_cast`
-           : `term10`
-   term10 : `term1` `args`
-          : @ `qualid` `universe_annot_opt` `term1_list_opt`
-          : `term1`
-   args : `args` `arg`
-        : `arg`
-   arg : ( `ident` := `term` )
-       : `term1`
-   term1_list_opt : `term1_list_opt` `term1`
-                  : `empty`
-   empty :
-   term1 : `term_projection`
-         : `term0` % `ident`
-         : `term0`
-   args_opt : `args`
-            : `empty`
-   term0 : `qualid` `universe_annot_opt`
-         : `sort`
-         : `numeral`
-         : `string`
-         : _
-         : `term_evar`
-         : `term_match`
-         : ( `term` )
-         : {| `fields_def` |}
-         : `{ `term` }
-         : `( `term` )
-         : ltac : ( `ltac_expr` )
-   fields_def : `field_def` ; `fields_def`
-              : `field_def`
-              : `empty`
-   field_def : `qualid` `binders_opt` := `term`
-   binders_opt : `binders`
-               : `empty`
+.. insertprodn term field_def
+
+.. prodn::
+   term ::= forall @open_binders , @term
+   | fun @open_binders => @term
+   | @term_let
+   | if @term {? {? as @name } return @term100 } then @term else @term
+   | @term_fix
+   | @term_cofix
+   | @term100
+   term100 ::= @term_cast
+   | @term10
+   term10 ::= @term1 {+ @arg }
+   | @ @qualid {? @univ_annot } {* @term1 }
+   | @term1
+   arg ::= ( @ident := @term )
+   | @term1
+   term1 ::= @term_projection
+   | @term0 % @ident
+   | @term0
+   term0 ::= @qualid {? @univ_annot }
+   | @sort
+   | @numeral
+   | @string
+   | _
+   | @term_evar
+   | @term_match
+   | ( @term )
+   | %{%| {* @field_def } %|%}
+   | `%{ @term %}
+   | `( @term )
+   | ltac : ( @ltac_expr )
+   field_def ::= @qualid {* @binder } := @term
 
 Types
 -----
@@ -196,12 +187,11 @@ of types inside the syntactic class :token:`term`.
 Qualified identifiers and simple identifiers
 --------------------------------------------
 
-.. insertgram qualid field
+.. insertprodn qualid field_ident
 
-.. productionlist:: coq
-   qualid : `qualid` `field`
-          : `ident`
-   field : .`ident`
+.. prodn::
+   qualid ::= @ident {* @field_ident }
+   field_ident ::= .@ident
 
 *Qualified identifiers* (:token:`qualid`) denote *global constants*
 (definitions, lemmas, theorems, remarks or facts), *global variables*
@@ -210,7 +200,7 @@ types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset
 of qualified identifiers. Identifiers may also denote *local variables*,
 while qualified identifiers do not.
 
-Field identifiers, written :token:`field`, are identifiers prefixed by
+Field identifiers, written :token:`field_ident`, are identifiers prefixed by
 `.` (dot) with no blank between the dot and the identifier.
 
 
@@ -237,34 +227,27 @@ numbers (see :ref:`datatypes`).
 Sorts
 -----
 
-.. insertgram sort universe_level
-
-.. productionlist:: coq
-   sort : Set
-        : Prop
-        : SProp
-        : Type
-        : Type @{ _ }
-        : Type @{ `universe` }
-   universe : max ( `universe_exprs_comma` )
-            : `universe_expr`
-   universe_exprs_comma : `universe_exprs_comma` , `universe_expr`
-                        : `universe_expr`
-   universe_expr : `universe_name` `universe_increment_opt`
-   universe_name : `qualid`
-                 : Set
-                 : Prop
-   universe_increment_opt : + `num`
-                          : `empty`
-   universe_annot_opt : @{ `universe_levels_opt` }
-                      : `empty`
-   universe_levels_opt : `universe_levels_opt` `universe_level`
-                       : `empty`
-   universe_level : Set
-                  : Prop
-                  : Type
-                  : _
-                  : `qualid`
+.. insertprodn sort univ_annot
+
+.. prodn::
+   sort ::= Set
+   | Prop
+   | SProp
+   | Type
+   | Type @%{ _ %}
+   | Type @%{ @universe %}
+   universe ::= max ( {+, @universe_expr } )
+   | @universe_expr
+   universe_expr ::= @universe_name {? + @num }
+   universe_name ::= @qualid
+   | Set
+   | Prop
+   universe_level ::= Set
+   | Prop
+   | Type
+   | _
+   | @qualid
+   univ_annot ::= @%{ {* @universe_level } %}
 
 There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set`  and :g:`Type`.
 
@@ -272,12 +255,12 @@ There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set`  and :g:`Type`.
    propositions* (also called *strict propositions*).
 
 -  :g:`Prop` is the universe of *logical propositions*. The logical propositions
-   themselves are typing the proofs. We denote propositions by :production:`form`.
+   themselves are typing the proofs. We denote propositions by :token:`form`.
    This constitutes a semantic subclass of the syntactic class :token:`term`.
 
 -  :g:`Set` is the universe of *program types* or *specifications*. The
    specifications themselves are typing the programs. We denote
-   specifications by :production:`specif`. This constitutes a semantic subclass of
+   specifications by :token:`specif`. This constitutes a semantic subclass of
    the syntactic class :token:`term`.
 
 -  :g:`Type` is the type of sorts.
@@ -289,34 +272,24 @@ More on sorts can be found in Section :ref:`sorts`.
 Binders
 -------
 
-.. insertgram open_binders exclam_opt
-
-.. productionlist:: coq
-   open_binders : `names` : `term`
-                : `binders`
-   names : `names` `name`
-         : `name`
-   name : _
-        : `ident`
-   binders : `binders` `binder`
-           : `binder`
-   binder : `name`
-          : ( `names` : `term` )
-          : ( `name` `colon_term_opt` := `term` )
-          : { `name` }
-          : { `names` `colon_term_opt` }
-          : `( `typeclass_constraints_comma` )
-          : `{ `typeclass_constraints_comma` }
-          : ' `pattern0`
-          : ( `name` : `term` | `term` )
-   typeclass_constraints_comma : `typeclass_constraints_comma` , `typeclass_constraint`
-                               : `typeclass_constraint`
-   typeclass_constraint : `exclam_opt` `term`
-                        : { `name` } : `exclam_opt` `term`
-                        : `name` : `exclam_opt` `term`
-   exclam_opt : !
-              : `empty`
-
+.. insertprodn open_binders typeclass_constraint
+
+.. prodn::
+   open_binders ::= {+ @name } : @term
+   | {+ @binder }
+   name ::= _
+   | @ident
+   binder ::= @name
+   | ( {+ @name } : @term )
+   | ( @name {? : @term } := @term )
+   | %{ {+ @name } {? : @term } %}
+   | `( {+, @typeclass_constraint } )
+   | `%{ {+, @typeclass_constraint } %}
+   | ' @pattern0
+   | ( @name : @term %| @term )
+   typeclass_constraint ::= {? ! } @term
+   | %{ @name %} : {? ! } @term
+   | @name : {? ! } @term
 
 Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix`
 *bind* variables. A binding is represented by an identifier. If the binding
@@ -411,13 +384,13 @@ Section :ref:`explicit-applications`).
 Type cast
 ---------
 
-.. insertgram term_cast term_cast
+.. insertprodn term_cast term_cast
 
-.. productionlist:: coq
-   term_cast : `term10` <: `term`
-             : `term10` <<: `term`
-             : `term10` : `term`
-             : `term10` :>
+.. prodn::
+   term_cast ::= @term10 <: @term
+   | @term10 <<: @term
+   | @term10 : @term
+   | @term10 :>
 
 The expression :n:`@term : @type` is a type cast expression. It enforces
 the type of :token:`term` to be :token:`type`.
@@ -444,21 +417,14 @@ guess the missing piece of information.
 Let-in definitions
 ------------------
 
-.. insertgram term_let names_comma
+.. insertprodn term_let term_let
 
-.. productionlist:: coq
-   term_let : let `name` `colon_term_opt` := `term` in `term`
-            : let `name` `binders` `colon_term_opt` := `term` in `term`
-            : let `single_fix` in `term`
-            : let `names_tuple` `as_return_type_opt` := `term` in `term`
-            : let ' `pattern` := `term` `return_type_opt` in `term`
-            : let ' `pattern` in `pattern` := `term` `return_type` in `term`
-   colon_term_opt : : `term`
-                  : `empty`
-   names_tuple : ( `names_comma` )
-               : ()
-   names_comma : `names_comma` , `name`
-               : `name`
+.. prodn::
+   term_let ::= let @name {? : @term } := @term in @term
+   | let @name {+ @binder } {? : @term } := @term in @term
+   | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
+   | let ' @pattern := @term {? return @term100 } in @term
+   | let ' @pattern in @pattern := @term return @term100 in @term
 
 :n:`let @ident := @term in @term’`
 denotes the local binding of :token:`term` to the variable
@@ -471,57 +437,25 @@ stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
 Definition by cases: match
 --------------------------
 
-.. insertgram term_match record_pattern
-
-.. productionlist:: coq
-   term_match : match `case_items_comma` `return_type_opt` with `or_opt` `eqns_or_opt` end
-   case_items_comma : `case_items_comma` , `case_item`
-                    : `case_item`
-   return_type_opt : `return_type`
-                   : `empty`
-   as_return_type_opt : `as_name_opt` `return_type`
-                      : `empty`
-   return_type : return `term100`
-   case_item : `term100` `as_name_opt` `in_opt`
-   as_name_opt : as `name`
-               : `empty`
-   in_opt : in `pattern`
-          : `empty`
-   or_opt : |
-          : `empty`
-   eqns_or_opt : `eqns_or`
-               : `empty`
-   eqns_or : `eqns_or` | `eqn`
-           : `eqn`
-   eqn : `patterns_comma_list_or` => `term`
-   patterns_comma_list_or : `patterns_comma_list_or` | `patterns_comma`
-                          : `patterns_comma`
-   patterns_comma : `patterns_comma` , `pattern`
-                  : `pattern`
-   pattern : `pattern10` : `term`
-           : `pattern10`
-   pattern10 : `pattern1` as `name`
-             : `pattern1_list`
-             : @ `qualid` `pattern1_list_opt`
-             : `pattern1`
-   pattern1_list : `pattern1_list` `pattern1`
-                 : `pattern1`
-   pattern1_list_opt : `pattern1_list`
-                     : `empty`
-   pattern1 : `pattern0` % `ident`
-            : `pattern0`
-   pattern0 : `qualid`
-            : {| `record_patterns_opt` |}
-            : _
-            : ( `patterns_or` )
-            : `numeral`
-            : `string`
-   patterns_or : `patterns_or` | `pattern`
-               : `pattern`
-   record_patterns_opt : `record_patterns_opt` ; `record_pattern`
-                       : `record_pattern`
-                       : `empty`
-   record_pattern : `qualid` := `pattern`
+.. insertprodn term_match pattern0
+
+.. prodn::
+   term_match ::= match {+, @case_item } {? return @term100 } with {? %| } {*| @eqn } end
+   case_item ::= @term100 {? as @name } {? in @pattern }
+   eqn ::= {+| {+, @pattern } } => @term
+   pattern ::= @pattern10 : @term
+   | @pattern10
+   pattern10 ::= @pattern1 as @name
+   | @pattern1 {* @pattern1 }
+   | @ @qualid {* @pattern1 }
+   pattern1 ::= @pattern0 % @ident
+   | @pattern0
+   pattern0 ::= @qualid
+   | %{%| {* @qualid := @pattern } %|%}
+   | _
+   | ( {+| @pattern } )
+   | @numeral
+   | @string
 
 Objects of inductive types can be destructured by a case-analysis
 construction called *pattern matching* expression. A pattern matching
@@ -531,31 +465,30 @@ to apply specific treatments accordingly.
 This paragraph describes the basic form of pattern matching. See
 Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
 of the general form. The basic form of pattern matching is characterized
-by a single :token:`case_item` expression, a :token:`patterns_comma` restricted to a
+by a single :token:`case_item` expression, an :token:`eqn` restricted to a
 single :token:`pattern` and :token:`pattern` restricted to the form
 :n:`@qualid {* @ident}`.
 
-The expression match ":token:`term`:math:`_0` :token:`return_type_opt` with
-:token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|`
-:token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a
-*pattern matching* over the term :token:`term`:math:`_0` (expected to be
-of an inductive type :math:`I`). The terms :token:`term`:math:`_1`\ …\
-:token:`term`:math:`_n` are the *branches* of the pattern matching
-expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid`
-:token:`ident` where :token:`qualid` must denote a constructor. There should be
+The expression
+:n:`match @term {? return @term100 } with {+| @pattern__i => @term__i } end` denotes a
+*pattern matching* over the term :n:`@term` (expected to be
+of an inductive type :math:`I`). The :n:`@term__i`
+are the *branches* of the pattern matching
+expression. Each :n:`@pattern__i` has the form :n:`@qualid @ident`
+where :n:`@qualid` must denote a constructor. There should be
 exactly one branch for every constructor of :math:`I`.
 
-The :token:`return_type_opt` expresses the type returned by the whole match
+The :n:`return @term100` clause gives the type returned by the whole match
 expression. There are several cases. In the *non dependent* case, all
-branches have the same type, and the :token:`return_type_opt` is the common type of
-branches. In this case, :token:`return_type_opt` can usually be omitted as it can be
-inferred from the type of the branches [2]_.
+branches have the same type, and the :n:`return @term100` specifies that type.
+In this case, :n:`return @term100` can usually be omitted as it can be
+inferred from the type of the branches [1]_.
 
 In the *dependent* case, there are three subcases. In the first subcase,
 the type in each branch may depend on the exact value being matched in
 the branch. In this case, the whole pattern matching itself depends on
 the term being matched. This dependency of the term being matched in the
-return type is expressed with an “as :token:`ident`” clause where :token:`ident`
+return type is expressed with an :n:`@ident` clause where :token:`ident`
 is dependent in the return type. For instance, in the following example:
 
 .. coqtop:: in
@@ -604,19 +537,19 @@ type of each branch can depend on the type dependencies specific to the
 branch and the whole pattern matching expression has a type determined
 by the specific dependencies in the type of the term being matched. This
 dependency of the return type in the annotations of the inductive type
-is expressed using a “:g:`in` :math:`I` :g:`_ … _` :token:`pattern`:math:`_1` …
-:token:`pattern`:math:`_n`” clause, where
+is expressed with a clause in the form
+:n:`in @qualid {+ _ } {+ @pattern }`, where
 
--  :math:`I` is the inductive type of the term being matched;
+-  :token:`qualid` is the inductive type of the term being matched;
 
--  the :g:`_` are matching the parameters of the inductive type: the
+-  the holes :n:`_` match the parameters of the inductive type: the
    return type is not dependent on them.
 
--  the :token:`pattern`:math:`_i` are matching the annotations of the
+-  each :n:`@pattern` matches the annotations of the
    inductive type: the return type is dependent on them
 
--  in the basic case which we describe below, each :token:`pattern`:math:`_i`
-   is a name :token:`ident`:math:`_i`; see :ref:`match-in-patterns` for the
+-  in the basic case which we describe below, each :n:`@pattern`
+   is a name :n:`@ident`; see :ref:`match-in-patterns` for the
    general case
 
 For instance, in the following example:
@@ -651,27 +584,18 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`).
 Recursive and co-recursive functions: fix and cofix
 ---------------------------------------------------
 
-.. insertgram term_fix term1_extended_opt
+.. insertprodn term_fix term1_extended
+
+.. prodn::
+   term_fix ::= let fix @fix_body in @term
+   | fix @fix_body {? {+ with @fix_body } for @ident }
+   fix_body ::= @ident {* @binder } {? @fixannot } {? : @term } := @term
+   fixannot ::= %{ struct @ident %}
+   | %{ wf @term1_extended @ident %}
+   | %{ measure @term1_extended {? @ident } {? @term1_extended } %}
+   term1_extended ::= @term1
+   | @ @qualid {? @univ_annot }
 
-.. productionlist:: coq
-   term_fix : `single_fix`
-            : `single_fix` with `fix_bodies` for `ident`
-   single_fix : fix `fix_body`
-              : cofix `fix_body`
-   fix_bodies : `fix_bodies` with `fix_body`
-              : `fix_body`
-   fix_body : `ident` `binders_opt` `fixannot_opt` `colon_term_opt` := `term`
-   fixannot_opt : `fixannot`
-                : `empty`
-   fixannot : { struct `ident` }
-            : { wf `term1_extended` `ident` }
-            : { measure `term1_extended` `ident_opt` `term1_extended_opt` }
-   term1_extended : `term1`
-                  : @ `qualid` `universe_annot_opt`
-   ident_opt : `ident`
-             : `empty`
-   term1_extended_opt : `term1_extended`
-                      : `empty`
 
 The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:``
 :token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` ``with … with``
@@ -681,6 +605,17 @@ The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:
 recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When
 :math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted.
 
+The association of a single fixpoint and a local definition have a special
+syntax: :n:`let fix @ident @binders := @term in` stands for
+:n:`let @ident := fix @ident @binders := @term in`. The same applies for co-fixpoints.
+
+.. insertprodn term_cofix cofix_body
+
+.. prodn::
+   term_cofix ::= let cofix @cofix_body in @term
+   | cofix @cofix_body {? {+ with @cofix_body } for @ident }
+   cofix_body ::= @ident {* @binder } {? : @term } := @term
+
 The expression “``cofix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:``
 :token:`type`:math:`_1` ``with … with`` :token:`ident`:math:`_n` :token:`binder`:math:`_n`
 : :token:`type`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the
@@ -688,10 +623,6 @@ The expression “``cofix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` `
 co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When
 :math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted.
 
-The association of a single fixpoint and a local definition have a special
-syntax: :n:`let fix @ident @binders := @term in` stands for
-:n:`let @ident := fix @ident @binders := @term in`. The same applies for co-fixpoints.
-
 .. _vernacular:
 
 The Vernacular
@@ -715,6 +646,8 @@ The Vernacular
                       : ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` )
    definition         : [Local] Definition `ident` [`binders`] [: `term`] := `term` .
                       : Let `ident` [`binders`] [: `term`] := `term` .
+   binders            : binders binder
+                      : binder
    inductive          : Inductive `ind_body` with … with `ind_body` .
                       : CoInductive `ind_body` with … with `ind_body` .
    ind_body           : `ident` [`binders`] : `term` :=
@@ -1715,10 +1648,5 @@ variety of commands:
    command with some attribute it does not understand.
 
 .. [1]
-   This is similar to the expression “*entry* :math:`\{` sep *entry*
-   :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry*
-   :math:`)`\ \*” in the syntax of regular expressions.
-
-.. [2]
    Except if the inductive type is empty in which case there is no
    equation that can be used to infer the return type.