Convert productionlists to prodns

7 files changed, 644 insertions, 1551 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index b9faeacad7..1f9178f4b6 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -403,13 +403,12 @@ class TableObject(NotationObject):
 class ProductionObject(CoqObject):
     r"""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::
 
@@ -418,7 +417,8 @@ class ProductionObject(CoqObject):
         | 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/tools/docgram/README.md b/doc/tools/docgram/README.md
index a0a1809133..182532e413 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -194,14 +194,15 @@ to the grammar.
 
 ### `.rst` file updates
 
-`doc_grammar` updates `.rst` files when it sees the following 3 lines
+`doc_grammar` updates `.rst` files where it sees the following 3 lines
 
 ```
-.. insertgram <start> <end>
-.. productionlist:: XXX
+.. insertprodn <start> <end>
+
+.. prodn::
 ```
 
-The end of the existing `productionlist` is recognized by a blank line.
+The end of the existing `prodn` is recognized by a blank line.
 
 ### Other details
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 06b49a0a18..9c1827f5b7 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -65,6 +65,7 @@ DELETE: [
 | test_lpar_idnum_coloneq
 | test_nospace_pipe_closedcurly
 | test_show_goal
+| ensure_fixannot
 
   (* SSR *)
 (* | ssr_null_entry *)
@@ -101,18 +102,8 @@ hyp: [
 | var
 ]
 
-empty: [
-|
-]
-
-or_opt: [
-| "|"
-| empty
-]
-
 ltac_expr_opt: [
-| tactic_expr5
-| empty
+| OPT tactic_expr5
 ]
 
 ltac_expr_opt_list_or: [
@@ -124,7 +115,7 @@ tactic_then_gen: [
 | EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
 | EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
 | REPLACE OPT tactic_expr5 ".." tactic_then_last
-| WITH ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
+| WITH ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
 ]
 
 ltac_expr_opt_list_or: [
@@ -144,24 +135,23 @@ fullyqualid: [
 | qualid
 ]
 
-
-field: [ | DELETENT ]
-
-field: [
+field_ident: [
 | "." ident
 ]
 
 basequalid: [
 | REPLACE ident fields
-| WITH qualid field
+| WITH ident LIST0 field_ident
+| DELETE ident
 ]
 
+field: [ | DELETENT ]
 fields: [ | DELETENT ]
 
 dirpath: [
 | REPLACE ident LIST0 field
 | WITH ident
-| dirpath field
+| dirpath field_ident
 ]
 
 binders: [
@@ -172,45 +162,37 @@ lconstr: [
 | DELETE l_constr
 ]
 
-let_type_cstr: [
-| DELETE OPT [ ":" lconstr ]
-| rec_type_cstr
+type_cstr: [
+| REPLACE ":" lconstr
+| WITH OPT ( ":" lconstr )
+| DELETE (* empty *)
 ]
 
-as_name_opt: [
-| "as" name
-| empty
+let_type_cstr: [
+| DELETE OPT [ ":" lconstr ]
+| type_cstr
 ]
 
 (* rename here because we want to use "return_type" for something else *)
 RENAME: [
-| return_type as_return_type_opt
-]
-
-as_return_type_opt: [
-| REPLACE OPT [ OPT [ "as" name ] case_type ]
-| WITH as_name_opt case_type
-| empty
+| return_type as_return_type
 ]
 
 case_item: [
 | REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
-| WITH operconstr100 as_name_opt OPT [ "in" pattern200 ]
-]
-
-as_dirpath: [
-| DELETE OPT [ "as" dirpath ]
-| "as" dirpath
-| empty
+| WITH operconstr100 OPT ("as" name) OPT [ "in" pattern200 ]
 ]
 
 binder_constr: [
 | MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
-| MOVETO term_let "let" single_fix "in" operconstr200
-| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| MOVETO term_fix "let" "fix" fix_decl "in" operconstr200
+| MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200
+| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
 | MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
 | MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
 | MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
+| MOVETO term_fix "fix" fix_decls
+| MOVETO term_cofix "cofix" cofix_decls
 ]
 
 term_let: [
@@ -218,8 +200,8 @@ term_let: [
 | WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200
 | "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200
 (* Don't need to document that "( )" is equivalent to "()" *)
-| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
-| WITH "let" [ "(" LIST1 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
+| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
+| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" operconstr200 "in" operconstr200
 | REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
 | WITH  "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200
 | DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
@@ -228,6 +210,8 @@ term_let: [
 atomic_constr: [
 (* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
 (* | DELETE string *)
+| REPLACE global univ_instance
+| WITH global OPT univ_instance
 | REPLACE "?" "[" ident "]"
 | WITH "?[" ident "]"
 | MOVETO term_evar "?[" ident "]"
@@ -253,6 +237,8 @@ operconstr10: [
 (* fixme: add in as a prodn somewhere *)
 | MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
 | DELETE dangling_pattern_extension_rule
+| REPLACE "@" global univ_instance LIST0 operconstr9
+| WITH "@" global OPT univ_instance LIST0 operconstr9
 ]
 
 operconstr9: [
@@ -260,64 +246,45 @@ operconstr9: [
 | DELETE ".." operconstr0 ".."
 ]
 
-arg_list: [
-| arg_list appl_arg
-| appl_arg
-]
-
-arg_list_opt: [
-| arg_list
-| empty
-]
-
 operconstr1: [
 | REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
-| WITH operconstr0 ".(" global arg_list_opt ")"
-| MOVETO term_projection operconstr0 ".(" global arg_list_opt ")"
+| WITH operconstr0 ".(" global LIST0 appl_arg ")"
+| MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
 | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
 ]
 
 operconstr0: [
 (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
 | DELETE "{" binder_constr "}"
+| REPLACE "{|" record_declaration bar_cbrace
+| WITH "{|" LIST0 field_def bar_cbrace
 ]
 
-single_fix: [
-| DELETE fix_kw fix_decl
-| "fix" fix_decl
-| "cofix" fix_decl
+fix_decls: [
+| DELETE fix_decl
+| REPLACE fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
+| WITH fix_decl OPT ( LIST1 ("with" fix_decl) "for" identref )
 ]
 
-fix_kw: [ | DELETENT ]
+cofix_decls: [
+| DELETE cofix_decl
+| REPLACE cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref
+| WITH cofix_decl OPT ( LIST1 ( "with" cofix_decl ) "for" identref )
+]
 
-binders_fixannot: [
-(*
-| REPLACE impl_name_head impl_ident_tail binders_fixannot
-| WITH impl_name_head impl_ident_tail "}" binders_fixannot
-*)
-(* Omit this complex detail.  See https://github.com/coq/coq/pull/10614#discussion_r344118146 *)
-| DELETE impl_name_head impl_ident_tail binders_fixannot
+fields_def: [
+| REPLACE field_def ";" fields_def
+| WITH LIST1 field_def SEP ";"
+| DELETE field_def
+]
 
-| DELETE fixannot
+binders_fixannot: [
 | DELETE binder binders_fixannot
+| DELETE fixannot
 | DELETE (* empty *)
-
 | LIST0 binder OPT fixannot
 ]
 
-impl_ident_tail: [
-| DELETENT
-(*
-| REPLACE "}"
-| WITH empty
-| REPLACE LIST1 name ":" lconstr "}"
-| WITH LIST1 name ":" lconstr
-| REPLACE LIST1 name "}"
-| WITH LIST1 name
-| REPLACE ":" lconstr "}"
-| WITH ":" lconstr
-*)
-]
 
 of_type_with_opt_coercion: [
 | DELETE ":>" ">"
@@ -347,18 +314,28 @@ closed_binder: [
 | DELETE "(" name ":" lconstr ")"
 
 | DELETE "(" name ":=" lconstr ")"
+
 | REPLACE "(" name ":" lconstr ":=" lconstr ")"
-| WITH "(" name rec_type_cstr ":=" lconstr ")"
+| WITH "(" name type_cstr ":=" lconstr ")"
 
+| DELETE "{" name "}"
 | DELETE "{" name LIST1 name "}"
 
 | REPLACE "{" name LIST1 name ":" lconstr "}"
-| WITH "{" LIST1 name rec_type_cstr "}"
+| WITH "{" LIST1 name type_cstr "}"
 | DELETE "{" name ":" lconstr  "}"
 ]
 
+name_colon: [
+| name ":"
+]
+
 typeclass_constraint: [
 | EDIT ADD_OPT "!" operconstr200
+| REPLACE "{" name "}" ":" [ "!" | ] operconstr200
+| WITH "{" name "}" ":" OPT "!"  operconstr200
+| REPLACE name_colon [ "!" | ] operconstr200
+| WITH name_colon OPT "!" operconstr200
 ]
 
 (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
@@ -376,62 +353,54 @@ DELETE: [
 | orient_rw
 ]
 
-pattern1_list: [
-| pattern1_list pattern1
-| pattern1
-]
-
-pattern1_list_opt: [
-| pattern1_list
-| empty
-]
-
 pattern10: [
 | REPLACE pattern1 LIST1 pattern1
-| WITH LIST1 pattern1
-| REPLACE "@" reference LIST0 pattern1
-| WITH "@" reference pattern1_list_opt
+| WITH pattern1 LIST0 pattern1
+| DELETE pattern1
 ]
 
 pattern0: [
 | REPLACE "(" pattern200 ")"
 | WITH "(" LIST1 pattern200 SEP "|" ")"
 | DELETE "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
+| REPLACE "{|" record_patterns bar_cbrace
+| WITH "{|" LIST0 record_pattern bar_cbrace
 ]
 
-patterns_comma: [
-| patterns_comma "," pattern100
-| pattern100
-]
-
-patterns_comma_list_or: [
-| patterns_comma_list_or "|" patterns_comma
-| patterns_comma
+DELETE: [
+| record_patterns
 ]
 
 eqn: [
 | REPLACE LIST1 mult_pattern SEP "|" "=>" lconstr
-| WITH patterns_comma_list_or "=>" lconstr
+| WITH LIST1 [ LIST1 pattern100 SEP "," ] SEP "|" "=>" lconstr
 ]
 
-record_patterns: [
-| REPLACE record_pattern ";" record_patterns
-| WITH record_patterns ";" record_pattern
+universe_increment: [
+| REPLACE "+" natural
+| WITH OPT ( "+" natural )
+| DELETE (* empty *)
 ]
 
-(* todo: binders should be binders_opt *)
-
+evar_instance: [
+| REPLACE "@{" LIST1 inst SEP ";" "}"
+| WITH OPT ( "@{" LIST1 inst SEP ";" "}" )
+| DELETE (* empty *)
+]
 
-(* lexer stuff *)
-bigint: [
-| DELETE NUMERAL
-| num
+univ_instance: [
+| DELETE (* empty *)
 ]
 
-ident: [
-| DELETENT
+constr: [
+| REPLACE "@" global univ_instance
+| WITH "@" global OPT univ_instance
 ]
 
+(* todo: binders should be binders_opt *)
+
+
+(* lexer stuff *)
 IDENT: [
 | ident
 ]
@@ -445,11 +414,45 @@ LEFTQMARK: [
 | "?"
 ]
 
+digit: [
+| "0" ".." "9"
+]
+
+num: [
+| LIST1 digit
+]
+
 natural: [ | DELETENT ]
 natural: [
 | num  (* todo: or should it be "nat"? *)
 ]
 
+numeral: [
+| LIST1 digit OPT ("." LIST1 digit) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
+]
+
+int: [
+| OPT "-" LIST1 digit
+]
+
+bigint: [
+| DELETE NUMERAL
+| num
+]
+
+first_letter: [
+| [ "a" ".." "z" | "A" ".." "Z" | "_" | unicode_letter ]
+]
+
+subsequent_letter: [
+| [ first_letter | digit | "'" | unicode_id_part ]
+]
+
+ident: [
+| DELETE IDENT
+| first_letter LIST0 subsequent_letter
+]
+
 NUMERAL: [
 | numeral
 ]
@@ -467,10 +470,6 @@ STRING: [
 
   (* added productions *)
 
-name_colon: [
-| name ":"
-]
-
 command_entry: [
 | noedit_mode
 ]
@@ -528,12 +527,6 @@ simple_tactic: [
 | WITH "eintros" intropatterns
 ]
 
-intropatterns: [
-| DELETE LIST0 intropattern
-| intropatterns intropattern
-| empty
-]
-
 (* todo: don't use DELETENT for this *)
 ne_intropatterns: [ | DELETENT ]
 
@@ -594,7 +587,6 @@ SPLICE: [
 | reference
 | bar_cbrace
 | lconstr
-| impl_name_head
 
 (*
 | ast_closure_term
@@ -665,6 +657,15 @@ SPLICE: [
 | name_colon
 | closed_binder
 | binders_fixannot
+| as_return_type
+| case_type
+| fields_def
+| universe_increment
+| type_cstr
+| record_pattern
+| evar_instance
+| fix_decls
+| cofix_decls
 ]
 
 RENAME: [
@@ -703,20 +704,13 @@ RENAME: [
 | BULLET bullet
 | nat_or_var num_or_var
 | fix_decl fix_body
-| instance universe_annot_opt
-| rec_type_cstr colon_term_opt
-| fix_constr term_fix
+| cofix_decl cofix_body
 | constr term1_extended
-| case_type return_type
 | appl_arg arg
-| record_patterns record_patterns_opt
-| universe_increment universe_increment_opt
 | rec_definition fix_definition
 | corec_definition cofix_definition
-| record_field_instance field_def
-| record_fields_instance fields_def
-| evar_instance evar_bindings_opt
 | inst evar_binding
+| univ_instance univ_annot
 ]
 
 
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 70976e705e..b50c427742 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -49,7 +49,7 @@ let default_args = {
 }
 
 let start_symbols = ["vernac_toplevel"]
-let tokens = [ "bullet"; "ident"; "int"; "num"; "numeral"; "string" ]
+let tokens = [ "bullet"; "string"; "unicode_id_part"; "unicode_letter" ]
 
 (* translated symbols *)
 
@@ -148,8 +148,10 @@ module DocGram = struct
 
   let g_add_prod_after g ins_after nt prod =
     let prods = try NTMap.find nt !g.map with Not_found -> [] in
-    (* todo: add check for duplicates *)
-    g_add_after g ~update:true ins_after nt (prods @ [prod])
+    if prods <> [] then
+      g_update_prods g nt (prods @ [prod])
+    else
+      g_add_after g ~update:true ins_after nt [prod]
 
   (* replace the map and order *)
   let g_reorder g map order =
@@ -237,7 +239,17 @@ and prod_to_str ?(plist=false) prod =
 
 
 let rec output_prodn = function
-  | Sterm s -> let s = if List.mem s ["{"; "{|"; "|"; "}"] then "%" ^ s else s in
+  | Sterm s ->
+    let s = match s with
+            | "|}" -> "%|%}"
+            | "{|" -> "%{%|"
+            | "`{" -> "`%{"
+            | "@{" -> "@%{"
+            | "{"
+            | "}"
+            | "|" -> "%" ^ s
+            | _ -> s
+    in
     sprintf "%s" s
   | Snterm s -> sprintf "@%s" s
   | Slist1 sym -> sprintf "{+ %s }" (output_prodn sym)
@@ -266,7 +278,14 @@ and output_sep sep =
   | Sterm s -> sprintf "%s" s  (* avoid escaping separator *)
   | _ -> output_prodn sep
 
-and prod_to_prodn prod = String.concat " " (List.map output_prodn prod)
+and prod_to_prodn_r prod =
+  match prod with
+  | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] ->
+    (sprintf "%s@ident" s) :: (prod_to_prodn_r tl)
+  | p :: tl -> (output_prodn p) :: (prod_to_prodn_r tl)
+  | [] -> []
+
+and prod_to_prodn prod = String.concat " " (prod_to_prodn_r prod)
 
 let pr_prods nt prods = (* duplicative *)
   Printf.printf "%s: [\n" nt;
@@ -304,11 +323,11 @@ let print_in_order out g fmt nt_order hide =
                 fprintf out "%s%s\n" pfx str)
               prods;
           | `PRODN ->
-            fprintf out "\n%s:\n" nt;
-            List.iter (fun prod ->
+            fprintf out "\n%s:\n%s " nt nt;
+            List.iteri (fun i prod ->
                 let str = prod_to_prodn prod in
-                let pfx = if str = "" then "" else " " in
-                fprintf out "%s%s\n" pfx str)
+                let op = if i = 0 then "::=" else "+=" in
+                fprintf out "%s %s\n" op str)
               prods;
         with Not_found -> error "Missing nt '%s' in print_in_order\n" nt)
     nt_order
@@ -458,8 +477,10 @@ let ematch prod edit =
           -> ematchr [psym] [sym] && ematchr [psep] [sep]
         | (Sparen psyml, Sparen syml)
           -> ematchr psyml syml
-        | (Sprod psymll, Sprod symll)
-          -> List.fold_left (&&) true (List.map2 ematchr psymll symll)
+        | (Sprod psymll, Sprod symll) ->
+          if List.compare_lengths psymll symll != 0 then false
+          else
+            List.fold_left (&&) true (List.map2 ematchr psymll symll)
         | _, _ -> phd = hd
       in
       m && ematchr ptl tl
@@ -691,17 +712,22 @@ let rec edit_prod g top edit_map prod =
       | _ -> [Snterm binding]
     with Not_found -> [sym0]
   in
+  let maybe_wrap syms =
+    match syms with
+    | s :: [] -> List.hd syms
+    | s -> Sparen (List.rev syms)
+  in
 
   let rec edit_symbol sym0 =
     match sym0 with
       | Sterm s -> [sym0]
       | Snterm s -> edit_nt edit_map sym0 s
-      | Slist1 sym -> [Slist1 (List.hd (edit_symbol sym))]
+      | Slist1 sym -> [Slist1 (maybe_wrap (edit_symbol sym))]
       (* you'll get a run-time failure deleting a SEP symbol *)
-      | Slist1sep (sym, sep) -> [Slist1sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))]
-      | Slist0 sym -> [Slist0 (List.hd (edit_symbol sym))]
-      | Slist0sep (sym, sep) -> [Slist0sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))]
-      | Sopt sym -> [Sopt (List.hd (edit_symbol sym))]
+      | Slist1sep (sym, sep) -> [Slist1sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))]
+      | Slist0 sym -> [Slist0 (maybe_wrap (edit_symbol sym))]
+      | Slist0sep (sym, sep) -> [Slist0sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))]
+      | Sopt sym -> [Sopt (maybe_wrap (edit_symbol sym))]
       | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))]
       | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in
                            [Sprod prods]
@@ -1079,7 +1105,9 @@ let apply_edit_file g edits =
             g_add_prod_after g (Some nt) nt2 oprod;
             let prods' = (try
               let posn = find_first oprod prods nt in
-              let prods = insert_after posn [[Snterm nt2]] prods in  (* insert new prod *)
+              let prods = if List.mem [Snterm nt2] prods then prods
+                else insert_after posn [[Snterm nt2]] prods (* insert new prod *)
+              in
               remove_prod oprod prods nt      (* remove orig prod *)
               with Not_found -> prods)
             in
@@ -1091,6 +1119,7 @@ let apply_edit_file g edits =
             aux tl (edit_single_prod g oprod prods nt) add_nt
           | (Snterm "REPLACE" :: oprod) :: (Snterm "WITH" :: rprod) :: tl ->
             report_undef_nts g rprod "";
+            (* todo: check result not already present *)
             let prods' = (try
               let posn = find_first oprod prods nt in
               let prods = insert_after posn [rprod] prods in  (* insert new prod *)
@@ -1580,7 +1609,7 @@ let process_rst g file args seen tac_prods cmd_prods =
     line
   in
   (* todo: maybe pass end_index? *)
-  let output_insertgram start_index end_ indent is_coq_group =
+  let output_insertprodn start_index end_ indent =
     let rec copy_prods list =
       match list with
       | [] -> ()
@@ -1590,21 +1619,21 @@ let process_rst g file args seen tac_prods cmd_prods =
           warn "%s line %d: '%s' already included at %s line %d\n"
               file !linenum nt prev_file prev_linenum;
         with Not_found ->
-          if is_coq_group then
-            seen := { !seen with nts = (NTMap.add nt (file, !linenum) !seen.nts)} );
+          seen := { !seen with nts = (NTMap.add nt (file, !linenum) !seen.nts)} );
         let prods = NTMap.find nt !g.map in
         List.iteri (fun i prod ->
-            let rhs = String.trim (sprintf ": %s" (prod_to_str ~plist:true prod)) in
-            fprintf new_rst "%s   %s %s\n" indent (if i = 0 then nt else String.make (String.length nt) ' ') rhs)
+            let rhs = String.trim (prod_to_prodn prod) in
+            let sep = if i = 0 then " ::=" else "|" in
+            fprintf new_rst "%s   %s%s %s\n" indent (if i = 0 then nt else "") sep rhs)
           prods;
         if nt <> end_ then copy_prods tl
     in
     copy_prods (nthcdr start_index !g.order)
   in
 
-  let process_insertgram line rhs =
+  let process_insertprodn line rhs =
     if not (Str.string_match ig_args_regex rhs 0) then
-      error "%s line %d: bad arguments '%s' for 'insertgram'\n" file !linenum rhs
+      error "%s line %d: bad arguments '%s' for 'insertprodn'\n" file !linenum rhs
     else begin
       let start = Str.matched_group 1 rhs in
       let end_ = Str.matched_group 2 rhs in
@@ -1624,19 +1653,18 @@ let process_rst g file args seen tac_prods cmd_prods =
           try
             let line2 = getline() in
             if not (Str.string_match blank_regex line2 0) then
-              error "%s line %d: expecting a blank line after 'insertgram'\n" file !linenum
+              error "%s line %d: expecting a blank line after 'insertprodn'\n" file !linenum
             else begin
               let line3 = getline() in
-              if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "productionlist::" then
-                error "%s line %d: expecting 'productionlist' after 'insertgram'\n" file !linenum
+              if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "prodn::" then
+                error "%s line %d: expecting 'prodn' after 'insertprodn'\n" file !linenum
               else begin
                 let indent = Str.matched_group 1 line3 in
-                let is_coq_group = ("coq" = String.trim (Str.matched_group 3 line3)) in
                 let rec skip_to_end () =
                   let endline = getline() in
                   if Str.string_match end_prodlist_regex endline 0 then begin
                     fprintf new_rst "%s\n\n%s\n" line line3;
-                    output_insertgram start_index end_ indent is_coq_group;
+                    output_insertprodn start_index end_ indent;
                     fprintf new_rst "%s\n" endline
                   end else
                     skip_to_end ()
@@ -1657,9 +1685,9 @@ let process_rst g file args seen tac_prods cmd_prods =
         let dir = Str.matched_group 2 line in
         let rhs = String.trim (Str.matched_group 3 line) in
         match dir with
-        | "productionlist::" ->
+        | "prodn::" ->
           if rhs = "coq" then
-            warn "%s line %d: Missing 'insertgram' before 'productionlist:: coq'\n" file !linenum;
+            warn "%s line %d: Missing 'insertprodn' before 'prodn:: coq'\n" file !linenum;
           fprintf new_rst "%s\n" line;
         | "tacn::" when args.check_tacs ->
           if not (StringSet.mem rhs tac_prods) then
@@ -1675,8 +1703,8 @@ let process_rst g file args seen tac_prods cmd_prods =
             warn "%s line %d: Repeated command: '%s'\n" file !linenum rhs;
           seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)};
           fprintf new_rst "%s\n" line
-        | "insertgram" ->
-          process_insertgram line rhs
+        | "insertprodn" ->
+          process_insertprodn line rhs
         | _ -> fprintf new_rst "%s\n" line
       end else
         fprintf new_rst "%s\n" line;
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ebaeb392a5..e12589bb89 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -64,7 +64,7 @@ lconstr: [
 
 constr: [
 | operconstr8
-| "@" global instance
+| "@" global univ_instance
 ]
 
 operconstr200: [
@@ -90,7 +90,7 @@ operconstr90: [
 
 operconstr10: [
 | operconstr9 LIST1 appl_arg
-| "@" global instance LIST0 operconstr9
+| "@" global univ_instance LIST0 operconstr9
 | "@" pattern_identref LIST1 identref
 | operconstr9
 ]
@@ -123,16 +123,16 @@ operconstr0: [
 ]
 
 record_declaration: [
-| record_fields_instance
+| fields_def
 ]
 
-record_fields_instance: [
-| record_field_instance ";" record_fields_instance
-| record_field_instance
+fields_def: [
+| field_def ";" fields_def
+| field_def
 |
 ]
 
-record_field_instance: [
+field_def: [
 | global binders ":=" lconstr
 ]
 
@@ -140,13 +140,15 @@ binder_constr: [
 | "forall" open_binders "," operconstr200
 | "fun" open_binders "=>" operconstr200
 | "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
-| "let" single_fix "in" operconstr200
+| "let" "fix" fix_decl "in" operconstr200
+| "let" "cofix" cofix_decl "in" operconstr200
 | "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200
 | "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
 | "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
 | "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
 | "if" operconstr200 return_type "then" operconstr200 "else" operconstr200
-| fix_constr
+| "fix" fix_decls
+| "cofix" cofix_decls
 ]
 
 appl_arg: [
@@ -155,7 +157,7 @@ appl_arg: [
 ]
 
 atomic_constr: [
-| global instance
+| global univ_instance
 | sort
 | NUMERAL
 | string
@@ -174,7 +176,7 @@ evar_instance: [
 |
 ]
 
-instance: [
+univ_instance: [
 | "@{" LIST0 universe_level "}"
 |
 ]
@@ -187,22 +189,22 @@ universe_level: [
 | global
 ]
 
-fix_constr: [
-| single_fix
-| single_fix "with" LIST1 fix_decl SEP "with" "for" identref
+fix_decls: [
+| fix_decl
+| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
 ]
 
-single_fix: [
-| fix_kw fix_decl
+cofix_decls: [
+| cofix_decl
+| cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref
 ]
 
-fix_kw: [
-| "fix"
-| "cofix"
+fix_decl: [
+| identref binders_fixannot type_cstr ":=" operconstr200
 ]
 
-fix_decl: [
-| identref binders_fixannot let_type_cstr ":=" operconstr200
+cofix_decl: [
+| identref binders type_cstr ":=" operconstr200
 ]
 
 match_constr: [
@@ -282,26 +284,14 @@ pattern0: [
 | string
 ]
 
-impl_ident_tail: [
-| "}"
-| LIST1 name ":" lconstr "}"
-| LIST1 name "}"
-| ":" lconstr "}"
-]
-
 fixannot: [
 | "{" "struct" identref "}"
 | "{" "wf" constr identref "}"
 | "{" "measure" constr OPT identref OPT constr "}"
 ]
 
-impl_name_head: [
-| impl_ident_head
-]
-
 binders_fixannot: [
-| impl_name_head impl_ident_tail binders_fixannot
-| fixannot
+| ensure_fixannot fixannot
 | binder binders_fixannot
 |
 ]
@@ -344,6 +334,11 @@ typeclass_constraint: [
 | operconstr200
 ]
 
+type_cstr: [
+| ":" lconstr
+|
+]
+
 let_type_cstr: [
 | OPT [ ":" lconstr ]
 ]
@@ -514,9 +509,6 @@ command: [
 | "Add" "LoadPath" ne_string as_dirpath
 | "Add" "Rec" "LoadPath" ne_string as_dirpath
 | "Remove" "LoadPath" ne_string
-| "AddPath" ne_string "as" as_dirpath
-| "AddRecPath" ne_string "as" as_dirpath
-| "DelPath" ne_string
 | "Type" lconstr
 | "Print" printable
 | "Print" smart_global OPT univ_name_list
@@ -963,16 +955,11 @@ opt_coercion: [
 ]
 
 rec_definition: [
-| ident_decl binders_fixannot rec_type_cstr OPT [ ":=" lconstr ] decl_notation
+| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
 ]
 
 corec_definition: [
-| ident_decl binders rec_type_cstr OPT [ ":=" lconstr ] decl_notation
-]
-
-rec_type_cstr: [
-| ":" lconstr
-|
+| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
 ]
 
 scheme: [
@@ -994,7 +981,6 @@ record_field: [
 
 record_fields: [
 | record_field ";" record_fields
-| record_field ";"
 | record_field
 |
 ]
@@ -1395,7 +1381,6 @@ syntax: [
 
 only_parsing: [
 | "(" "only" "parsing" ")"
-| "(" "compat" STRING ")"
 |
 ]
 
@@ -1413,7 +1398,6 @@ syntax_modifier: [
 | "no" "associativity"
 | "only" "printing"
 | "only" "parsing"
-| "compat" STRING
 | "format" STRING OPT STRING
 | IDENT; "," LIST1 IDENT SEP "," "at" level
 | IDENT; "at" level
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 545ccde03a..63e0ca129c 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -8,30 +8,15 @@ vernac_toplevel: [
 | "Quit" "."
 | "BackTo" num "."
 | "Show" "Goal" num "at" num "."
-| "Show" "Proof" "Diffs" removed_opt "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
 | vernac_control
 ]
 
-removed_opt: [
-| "removed"
-| empty
-]
-
 tactic_mode: [
-| toplevel_selector_opt query_command
-| toplevel_selector_opt "{"
-| toplevel_selector_opt ltac_info_opt ltac_expr ltac_use_default
-| "par" ":" ltac_info_opt ltac_expr ltac_use_default
-]
-
-toplevel_selector_opt: [
-| toplevel_selector
-| empty
-]
-
-ltac_info_opt: [
-| "Info" num
-| empty
+| OPT toplevel_selector query_command
+| OPT toplevel_selector "{"
+| OPT toplevel_selector OPT ( "Info" num ) ltac_expr ltac_use_default
+| "par" ":" OPT ( "Info" num ) ltac_expr ltac_use_default
 ]
 
 ltac_use_default: [
@@ -44,15 +29,16 @@ vernac_control: [
 | "Redirect" string vernac_control
 | "Timeout" num vernac_control
 | "Fail" vernac_control
-| quoted_attributes_list_opt vernac
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) vernac
 ]
 
 term: [
 | "forall" open_binders "," term
 | "fun" open_binders "=>" term
 | term_let
-| "if" term as_return_type_opt "then" term "else" term
+| "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
 | term_fix
+| term_cofix
 | term100
 ]
 
@@ -62,43 +48,24 @@ term100: [
 ]
 
 term10: [
-| term1 args
-| "@" qualid universe_annot_opt term1_list_opt
+| term1 LIST1 arg
+| "@" qualid OPT univ_annot LIST0 term1
 | 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
+| qualid OPT univ_annot
 | sort
 | numeral
 | string
@@ -106,46 +73,25 @@ term0: [
 | term_evar
 | term_match
 | "(" term ")"
-| "{|" fields_def "|}"
+| "{|" LIST0 field_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
+| qualid LIST0 binder ":=" term
 ]
 
 term_projection: [
-| term0 ".(" qualid args_opt ")"
-| term0 ".(" "@" qualid term1_list_opt ")"
+| term0 ".(" qualid LIST0 arg ")"
+| term0 ".(" "@" qualid LIST0 ( term1 ) ")"
 ]
 
 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
+| "?" ident OPT ( "@{" LIST1 evar_binding SEP ";" "}" )
 ]
 
 evar_binding: [
@@ -153,42 +99,26 @@ evar_binding: [
 ]
 
 dangling_pattern_extension_rule: [
-| "@" "?" ident ident_list
-]
-
-ident_list: [
-| ident_list ident
-| ident
+| "@" "?" ident LIST1 ident
 ]
 
 record_fields: [
 | record_field ";" record_fields
-| record_field ";"
 | record_field
-| empty
+|
 ]
 
 record_field: [
-| quoted_attributes_list_opt record_binder num_opt2 decl_notation
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) record_binder OPT [ "|" num ] decl_notation
 ]
 
 decl_notation: [
-| "where" one_decl_notation_list
-| empty
-]
-
-one_decl_notation_list: [
-| one_decl_notation_list "and" one_decl_notation
-| one_decl_notation
+| "where" LIST1 one_decl_notation SEP "and"
+|
 ]
 
 one_decl_notation: [
-| string ":=" term1_extended ident_opt3
-]
-
-ident_opt3: [
-| ":" ident
-| empty
+| string ":=" term1_extended OPT [ ":" ident ]
 ]
 
 record_binder: [
@@ -197,9 +127,9 @@ record_binder: [
 ]
 
 record_binder_body: [
-| binders_opt of_type_with_opt_coercion term
-| binders_opt of_type_with_opt_coercion term ":=" term
-| binders_opt ":=" term
+| LIST0 binder of_type_with_opt_coercion term
+| LIST0 binder of_type_with_opt_coercion term ":=" term
+| LIST0 binder ":=" term
 ]
 
 of_type_with_opt_coercion: [
@@ -208,43 +138,50 @@ of_type_with_opt_coercion: [
 | ":"
 ]
 
-num_opt2: [
-| "|" num
-| empty
+attribute: [
+| ident attribute_value
 ]
 
-quoted_attributes_list_opt: [
-| quoted_attributes_list_opt "#[" attribute_list_comma_opt "]"
-| empty
+attribute_value: [
+| "=" string
+| "(" LIST0 attribute SEP "," ")"
+|
 ]
 
-attribute_list_comma_opt: [
-| attribute_list_comma
-| empty
+qualid: [
+| ident LIST0 field_ident
 ]
 
-attribute_list_comma: [
-| attribute_list_comma "," attribute
-| attribute
+field_ident: [
+| "." ident
 ]
 
-attribute: [
-| ident attribute_value
+numeral: [
+| LIST1 digit OPT ( "." LIST1 digit ) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
 ]
 
-attribute_value: [
-| "=" string
-| "(" attribute_list_comma_opt ")"
-| empty
+int: [
+| OPT "-" LIST1 digit
 ]
 
-qualid: [
-| qualid field
-| ident
+num: [
+| LIST1 digit
 ]
 
-field: [
-| "." ident
+digit: [
+| "0" ".." "9"
+]
+
+ident: [
+| first_letter LIST0 subsequent_letter
+]
+
+first_letter: [
+| [ "a" ".." "z" | "A" ".." "Z" | "_" | unicode_letter ]
+]
+
+subsequent_letter: [
+| [ first_letter | digit | "'" | unicode_id_part ]
 ]
 
 sort: [
@@ -257,17 +194,12 @@ sort: [
 ]
 
 universe: [
-| "max" "(" universe_exprs_comma ")"
-| universe_expr
-]
-
-universe_exprs_comma: [
-| universe_exprs_comma "," universe_expr
+| "max" "(" LIST1 universe_expr SEP "," ")"
 | universe_expr
 ]
 
 universe_expr: [
-| universe_name universe_increment_opt
+| universe_name OPT ( "+" num )
 ]
 
 universe_name: [
@@ -276,21 +208,6 @@ universe_name: [
 | "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"
@@ -299,83 +216,50 @@ universe_level: [
 | qualid
 ]
 
-term_fix: [
-| single_fix
-| single_fix "with" fix_bodies "for" ident
-]
-
-single_fix: [
-| "fix" fix_body
-| "cofix" fix_body
+univ_annot: [
+| "@{" LIST0 universe_level "}"
 ]
 
-fix_bodies: [
-| fix_bodies "with" fix_body
-| fix_body
+term_fix: [
+| "let" "fix" fix_body "in" term
+| "fix" fix_body OPT ( LIST1 ( "with" fix_body ) "for" ident )
 ]
 
 fix_body: [
-| ident binders_opt fixannot_opt colon_term_opt ":=" term
-]
-
-fixannot_opt: [
-| fixannot
-| empty
+| ident LIST0 binder OPT fixannot OPT ( ":" term ) ":=" term
 ]
 
 fixannot: [
 | "{" "struct" ident "}"
 | "{" "wf" term1_extended ident "}"
-| "{" "measure" term1_extended ident_opt term1_extended_opt "}"
+| "{" "measure" term1_extended OPT ident OPT term1_extended "}"
 ]
 
 term1_extended: [
 | term1
-| "@" qualid universe_annot_opt
+| "@" qualid OPT univ_annot
 ]
 
-ident_opt: [
-| ident
-| empty
+term_cofix: [
+| "let" "cofix" cofix_body "in" term
+| "cofix" cofix_body OPT ( LIST1 ( "with" cofix_body ) "for" ident )
 ]
 
-term1_extended_opt: [
-| term1_extended
-| empty
+cofix_body: [
+| ident LIST0 binder OPT ( ":" term ) ":=" term
 ]
 
 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
+| "let" name OPT ( ":" term ) ":=" term "in" term
+| "let" name LIST1 binder OPT ( ":" term ) ":=" term "in" term
+| "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term
+| "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term
+| "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term
 ]
 
 open_binders: [
-| names ":" term
-| binders
-]
-
-names: [
-| names name
-| name
+| LIST1 name ":" term
+| LIST1 binder
 ]
 
 name: [
@@ -383,37 +267,21 @@ 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 "}"
+| "(" LIST1 name ":" term ")"
+| "(" name OPT ( ":" term ) ":=" term ")"
+| "{" LIST1 name OPT ( ":" term ) "}"
+| "`(" LIST1 typeclass_constraint SEP "," ")"
+| "`{" LIST1 typeclass_constraint SEP "," "}"
 | "'" 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
+| OPT "!" term
+| "{" name "}" ":" OPT "!" term
+| name ":" OPT "!" term
 ]
 
 term_cast: [
@@ -424,69 +292,15 @@ term_cast: [
 ]
 
 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
+| "match" LIST1 case_item SEP "," OPT ( "return" term100 ) "with" OPT "|" LIST0 eqn SEP "|" "end"
 ]
 
 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
+| term100 OPT ( "as" name ) OPT [ "in" pattern ]
 ]
 
 eqn: [
-| patterns_comma_list_or "=>" term
-]
-
-patterns_comma_list_or: [
-| patterns_comma_list_or "|" patterns_comma
-| patterns_comma
-]
-
-patterns_comma: [
-| patterns_comma "," pattern
-| pattern
+| LIST1 [ LIST1 pattern SEP "," ] SEP "|" "=>" term
 ]
 
 pattern: [
@@ -496,19 +310,8 @@ pattern: [
 
 pattern10: [
 | pattern1 "as" name
-| pattern1_list
-| "@" qualid pattern1_list_opt
-| pattern1
-]
-
-pattern1_list: [
-| pattern1_list pattern1
-| pattern1
-]
-
-pattern1_list_opt: [
-| pattern1_list
-| empty
+| pattern1 LIST0 pattern1
+| "@" qualid LIST0 pattern1
 ]
 
 pattern1: [
@@ -518,28 +321,13 @@ pattern1: [
 
 pattern0: [
 | qualid
-| "{|" record_patterns_opt "|}"
+| "{|" LIST0 ( qualid ":=" pattern ) "|}"
 | "_"
-| "(" patterns_or ")"
+| "(" LIST1 pattern SEP "|" ")"
 | numeral
 | string
 ]
 
-patterns_or: [
-| patterns_or "|" pattern
-| pattern
-]
-
-record_patterns_opt: [
-| record_patterns_opt ";" record_pattern
-| record_pattern
-| empty
-]
-
-record_pattern: [
-| qualid ":=" pattern
-]
-
 vernac: [
 | "Local" vernac_poly
 | "Global" vernac_poly
@@ -571,78 +359,28 @@ subprf: [
 ]
 
 gallina: [
-| thm_token ident_decl binders_opt ":" term with_list_opt
+| thm_token ident_decl LIST0 binder ":" term LIST0 [ "with" ident_decl LIST0 binder ":" term ]
 | assumption_token inline assum_list
 | assumptions_token inline assum_list
 | def_token ident_decl def_body
 | "Let" ident def_body
-| cumulativity_token_opt private_token finite_token inductive_definition_list
-| "Fixpoint" fix_definition_list
-| "Let" "Fixpoint" fix_definition_list
-| "CoFixpoint" cofix_definition_list
-| "Let" "CoFixpoint" cofix_definition_list
-| "Scheme" scheme_list
-| "Combined" "Scheme" ident "from" ident_list_comma
+| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
+| "Fixpoint" LIST1 fix_definition SEP "with"
+| "Let" "Fixpoint" LIST1 fix_definition SEP "with"
+| "CoFixpoint" LIST1 cofix_definition SEP "with"
+| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with"
+| "Scheme" LIST1 scheme SEP "with"
+| "Combined" "Scheme" ident "from" LIST1 ident SEP ","
 | "Register" qualid "as" qualid
 | "Register" "Inline" qualid
-| "Primitive" ident term_opt ":=" register_token
-| "Universe" ident_list
-| "Universes" ident_list
-| "Constraint" univ_constraint_list_comma
-]
-
-term_opt: [
-| ":" term
-| empty
-]
-
-univ_constraint_list_comma: [
-| univ_constraint_list_comma "," univ_constraint
-| univ_constraint
-]
-
-with_list_opt: [
-| with_list_opt "with" ident_decl binders_opt ":" term
-| empty
-]
-
-cumulativity_token_opt: [
-| cumulativity_token
-| empty
-]
-
-inductive_definition_list: [
-| inductive_definition_list "with" inductive_definition
-| inductive_definition
-]
-
-fix_definition_list: [
-| fix_definition_list "with" fix_definition
-| fix_definition
+| "Primitive" ident OPT [ ":" term ] ":=" register_token
+| "Universe" LIST1 ident
+| "Universes" LIST1 ident
+| "Constraint" LIST1 univ_constraint SEP ","
 ]
 
 fix_definition: [
-| ident_decl binders_opt fixannot_opt colon_term_opt term_opt2 decl_notation
-]
-
-term_opt2: [
-| ":=" term
-| empty
-]
-
-cofix_definition_list: [
-| cofix_definition_list "with" cofix_definition
-| cofix_definition
-]
-
-scheme_list: [
-| scheme_list "with" scheme
-| scheme
-]
-
-ident_list_comma: [
-| ident_list_comma "," ident
-| ident
+| ident_decl LIST0 binder OPT fixannot OPT ( ":" term ) OPT [ ":=" term ] decl_notation
 ]
 
 register_token: [
@@ -731,21 +469,15 @@ assumptions_token: [
 inline: [
 | "Inline" "(" num ")"
 | "Inline"
-| empty
+|
 ]
 
 univ_constraint: [
-| universe_name lt_alt universe_name
-]
-
-lt_alt: [
-| "<"
-| "="
-| "<="
+| universe_name [ "<" | "=" | "<=" ] universe_name
 ]
 
 ident_decl: [
-| ident univ_decl_opt
+| ident OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] )
 ]
 
 finite_token: [
@@ -764,46 +496,41 @@ cumulativity_token: [
 
 private_token: [
 | "Private"
-| empty
+|
 ]
 
 def_body: [
-| binders_opt ":=" reduce term
-| binders_opt ":" term ":=" reduce term
-| binders_opt ":" term
+| LIST0 binder ":=" reduce term
+| LIST0 binder ":" term ":=" reduce term
+| LIST0 binder ":" term
 ]
 
 reduce: [
 | "Eval" red_expr "in"
-| empty
+|
 ]
 
 red_expr: [
 | "red"
 | "hnf"
-| "simpl" delta_flag ref_or_pattern_occ_opt
+| "simpl" delta_flag OPT ref_or_pattern_occ
 | "cbv" strategy_flag
 | "cbn" strategy_flag
 | "lazy" strategy_flag
 | "compute" delta_flag
-| "vm_compute" ref_or_pattern_occ_opt
-| "native_compute" ref_or_pattern_occ_opt
-| "unfold" unfold_occ_list_comma
-| "fold" term1_extended_list
-| "pattern" pattern_occ_list_comma
+| "vm_compute" OPT ref_or_pattern_occ
+| "native_compute" OPT ref_or_pattern_occ
+| "unfold" LIST1 unfold_occ SEP ","
+| "fold" LIST1 term1_extended
+| "pattern" LIST1 pattern_occ SEP ","
 | ident
 ]
 
 strategy_flag: [
-| red_flags_list
+| LIST1 red_flags
 | delta_flag
 ]
 
-red_flags_list: [
-| red_flags_list red_flags
-| red_flags
-]
-
 red_flags: [
 | "beta"
 | "iota"
@@ -815,14 +542,9 @@ red_flags: [
 ]
 
 delta_flag: [
-| "-" "[" smart_global_list "]"
-| "[" smart_global_list "]"
-| empty
-]
-
-ref_or_pattern_occ_opt: [
-| ref_or_pattern_occ
-| empty
+| "-" "[" LIST1 smart_global "]"
+| "[" LIST1 smart_global "]"
+|
 ]
 
 ref_or_pattern_occ: [
@@ -830,83 +552,48 @@ ref_or_pattern_occ: [
 | term1_extended occs
 ]
 
-unfold_occ_list_comma: [
-| unfold_occ_list_comma "," unfold_occ
-| unfold_occ
-]
-
 unfold_occ: [
 | smart_global occs
 ]
 
-pattern_occ_list_comma: [
-| pattern_occ_list_comma "," pattern_occ
-| pattern_occ
-]
-
 opt_constructors_or_fields: [
 | ":=" constructor_list_or_record_decl
-| empty
+|
 ]
 
 inductive_definition: [
-| opt_coercion ident_decl binders_opt term_opt opt_constructors_or_fields decl_notation
+| opt_coercion ident_decl LIST0 binder OPT [ ":" term ] opt_constructors_or_fields decl_notation
 ]
 
 opt_coercion: [
 | ">"
-| empty
+|
 ]
 
 constructor_list_or_record_decl: [
-| "|" constructor_list_or
-| ident constructor_type "|" constructor_list_or_opt
+| "|" LIST1 constructor SEP "|"
+| ident constructor_type "|" LIST0 constructor SEP "|"
 | ident constructor_type
 | ident "{" record_fields "}"
 | "{" record_fields "}"
-| empty
-]
-
-constructor_list_or: [
-| constructor_list_or "|" constructor
-| constructor
-]
-
-constructor_list_or_opt: [
-| constructor_list_or
-| empty
+|
 ]
 
 assum_list: [
-| assum_coe_list
+| LIST1 assum_coe
 | simple_assum_coe
 ]
 
-assum_coe_list: [
-| assum_coe_list assum_coe
-| assum_coe
-]
-
 assum_coe: [
 | "(" simple_assum_coe ")"
 ]
 
 simple_assum_coe: [
-| ident_decl_list of_type_with_opt_coercion term
-]
-
-ident_decl_list: [
-| ident_decl_list ident_decl
-| ident_decl
+| LIST1 ident_decl of_type_with_opt_coercion term
 ]
 
 constructor_type: [
-| binders_opt of_type_with_opt_coercion_opt
-]
-
-of_type_with_opt_coercion_opt: [
-| of_type_with_opt_coercion term
-| empty
+| LIST0 binder [ of_type_with_opt_coercion term | ]
 ]
 
 constructor: [
@@ -914,7 +601,7 @@ constructor: [
 ]
 
 cofix_definition: [
-| ident_decl binders_opt colon_term_opt term_opt2 decl_notation
+| ident_decl LIST0 binder OPT ( ":" term ) OPT [ ":=" term ] decl_notation
 ]
 
 scheme: [
@@ -943,67 +630,47 @@ smart_global: [
 ]
 
 by_notation: [
-| string ident_opt2
-]
-
-ident_opt2: [
-| "%" ident
-| empty
+| string OPT [ "%" ident ]
 ]
 
 gallina_ext: [
-| "Module" export_token ident module_binder_list_opt of_module_type is_module_expr
-| "Module" "Type" ident module_binder_list_opt module_type_inl_list_opt is_module_type
-| "Declare" "Module" export_token ident module_binder_list_opt ":" module_type_inl
+| "Module" export_token ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) of_module_type is_module_expr
+| "Module" "Type" ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) LIST0 ( "<:" module_type_inl ) is_module_type
+| "Declare" "Module" export_token ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) ":" module_type_inl
 | "Section" ident
 | "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
-| "Require" export_token qualid_list
-| "From" qualid "Require" export_token qualid_list
-| "Import" qualid_list
-| "Export" qualid_list
-| "Include" module_type_inl module_expr_inl_list_opt
-| "Include" "Type" module_type_inl module_type_inl_list_opt
-| "Transparent" smart_global_list
-| "Opaque" smart_global_list
-| "Strategy" strategy_level_list
-| "Canonical" Structure_opt qualid univ_decl_opt2
-| "Canonical" Structure_opt by_notation
-| "Coercion" qualid univ_decl_opt def_body
+| "Require" export_token LIST1 qualid
+| "From" qualid "Require" export_token LIST1 qualid
+| "Import" LIST1 qualid
+| "Export" LIST1 qualid
+| "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
+| "Include" "Type" module_type_inl LIST0 ( "<+" module_type_inl )
+| "Transparent" LIST1 smart_global
+| "Opaque" LIST1 smart_global
+| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
+| "Canonical" OPT "Structure" qualid OPT [ OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body ]
+| "Canonical" OPT "Structure" by_notation
+| "Coercion" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body
 | "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
-| "Context" binders
-| "Instance" instance_name ":" term hint_info fields_def_opt
+| "Context" LIST1 binder
+| "Instance" instance_name ":" term hint_info [ ":=" "{" [ LIST1 field_def SEP ";" | ] "}" | ":=" term | ]
 | "Existing" "Instance" qualid hint_info
-| "Existing" "Instances" qualid_list num_opt2
+| "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
 | "Existing" "Class" qualid
-| "Arguments" smart_global argument_spec_block_list_opt more_implicits_block_opt arguments_modifier_opt
+| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
 | "Implicit" "Type" reserv_list
 | "Implicit" "Types" reserv_list
-| "Generalizable" All_alt
-| "Export" "Set" ident_list option_setting
-| "Export" "Unset" ident_list
-]
-
-smart_global_list: [
-| smart_global_list smart_global
-| smart_global
-]
-
-num_opt: [
-| num
-| empty
-]
-
-qualid_list: [
-| qualid_list qualid
-| qualid
+| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ]
+| "Export" "Set" LIST1 ident option_setting
+| "Export" "Unset" LIST1 ident
 ]
 
 option_setting: [
-| empty
+|
 | int
 | string
 ]
@@ -1015,132 +682,35 @@ class_rawexpr: [
 ]
 
 hint_info: [
-| "|" num_opt term1_extended_opt
-| empty
-]
-
-module_binder_list_opt: [
-| module_binder_list_opt "(" export_token ident_list ":" module_type_inl ")"
-| empty
-]
-
-module_type_inl_list_opt: [
-| module_type_inl_list_opt module_type_inl
-| empty
-]
-
-module_expr_inl_list_opt: [
-| module_expr_inl_list_opt module_expr_inl
-| empty
-]
-
-strategy_level_list: [
-| strategy_level_list strategy_level "[" smart_global_list "]"
-| strategy_level "[" smart_global_list "]"
-]
-
-fields_def_opt: [
-| ":=" "{" fields_def "}"
-| ":=" term
-| empty
-]
-
-argument_spec_block_list_opt: [
-| argument_spec_block_list_opt argument_spec_block
-| empty
-]
-
-more_implicits_block_opt: [
-| "," more_implicits_block_list_comma
-| empty
-]
-
-more_implicits_block_list_comma: [
-| more_implicits_block_list_comma "," more_implicits_block_list_opt
-| more_implicits_block_list_opt
-]
-
-arguments_modifier_opt: [
-| ":" arguments_modifier_list_comma
-| empty
-]
-
-arguments_modifier_list_comma: [
-| arguments_modifier_list_comma "," arguments_modifier
-| arguments_modifier
-]
-
-All_alt: [
-| "All" "Variables"
-| "No" "Variables"
-| Variable_alt ident_list
-]
-
-Variable_alt: [
-| "Variable"
-| "Variables"
-]
-
-more_implicits_block_list_opt: [
-| more_implicits_block_list_opt more_implicits_block
-| empty
-]
-
-univ_decl_opt2: [
-| univ_decl_opt def_body
-| empty
-]
-
-univ_decl_opt: [
-| "@{" ident_list_opt plus_opt univ_constraint_alt
-| empty
-]
-
-plus_opt: [
-| "+"
-| empty
-]
-
-univ_constraint_alt: [
-| "|" univ_constraint_list_comma_opt plus_opt "}"
-| rbrace_alt
-]
-
-univ_constraint_list_comma_opt: [
-| univ_constraint_list_comma
-| empty
-]
-
-rbrace_alt: [
-| "}"
-| "|}"
+| "|" OPT num OPT term1_extended
+|
 ]
 
 export_token: [
 | "Import"
 | "Export"
-| empty
+|
 ]
 
 of_module_type: [
 | ":" module_type_inl
-| module_type_inl_list_opt
+| LIST0 ( "<:" module_type_inl )
 ]
 
 is_module_type: [
-| ":=" module_type_inl module_type_inl_list_opt
-| empty
+| ":=" module_type_inl LIST0 ( "<+" module_type_inl )
+|
 ]
 
 is_module_expr: [
-| ":=" module_expr_inl module_expr_inl_list_opt
-| empty
+| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl )
+|
 ]
 
 functor_app_annot: [
 | "[" "inline" "at" "level" num "]"
 | "[" "no" "inline" "]"
-| empty
+|
 ]
 
 module_expr_inl: [
@@ -1171,33 +741,23 @@ module_type: [
 ]
 
 with_declaration: [
-| "Definition" qualid univ_decl_opt ":=" term
+| "Definition" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) ":=" term
 | "Module" qualid ":=" qualid
 ]
 
 argument_spec_block: [
-| exclam_opt name scope_delimiter_opt
+| OPT "!" name OPT ( "%" ident )
 | "/"
 | "&"
-| "(" scope_delimiter_list ")" scope_delimiter_opt
-| "[" scope_delimiter_list "]" scope_delimiter_opt
-| "{" scope_delimiter_list "}" scope_delimiter_opt
-]
-
-scope_delimiter_opt: [
-| "%" ident
-| empty
-]
-
-scope_delimiter_list: [
-| scope_delimiter_list scope_delimiter_opt
-| scope_delimiter_opt
+| "(" LIST1 ( OPT "!" name OPT ( "%" ident ) ) ")" OPT ( "%" ident )
+| "[" LIST1 ( OPT "!" name OPT ( "%" ident ) ) "]" OPT ( "%" ident )
+| "{" LIST1 ( OPT "!" name OPT ( "%" ident ) ) "}" OPT ( "%" ident )
 ]
 
 more_implicits_block: [
 | name
-| "[" names "]"
-| "{" names "}"
+| "[" LIST1 name "]"
+| "{" LIST1 name "}"
 ]
 
 strategy_level: [
@@ -1208,26 +768,21 @@ strategy_level: [
 ]
 
 instance_name: [
-| ident_decl binders_opt
-| empty
+| ident_decl LIST0 binder
+|
 ]
 
 reserv_list: [
-| reserv_tuple_list
+| LIST1 reserv_tuple
 | simple_reserv
 ]
 
-reserv_tuple_list: [
-| reserv_tuple_list reserv_tuple
-| reserv_tuple
-]
-
 reserv_tuple: [
 | "(" simple_reserv ")"
 ]
 
 simple_reserv: [
-| ident_list ":" term
+| LIST1 ident ":" term
 ]
 
 arguments_modifier: [
@@ -1244,46 +799,36 @@ arguments_modifier: [
 | "clear" "implicits" "and" "scopes"
 ]
 
-Structure_opt: [
-| "Structure"
-| empty
-]
-
 command: [
 | "Goal" term
-| "Comments" comment_list_opt
-| "Declare" "Instance" ident_decl binders_opt ":" term hint_info
 | "Declare" "Scope" ident
 | "Pwd"
 | "Cd"
 | "Cd" string
-| "Load" Verbose_opt string_alt
-| "Declare" "ML" "Module" string_list
+| "Load" [ "Verbose" | ] [ string | ident ]
+| "Declare" "ML" "Module" LIST1 string
 | "Locate" locatable
 | "Add" "LoadPath" string as_dirpath
 | "Add" "Rec" "LoadPath" string as_dirpath
 | "Remove" "LoadPath" string
-| "AddPath" string "as" as_dirpath
-| "AddRecPath" string "as" as_dirpath
-| "DelPath" string
 | "Type" term
 | "Print" printable
-| "Print" smart_global univ_name_list_opt
+| "Print" smart_global OPT ( "@{" LIST0 name "}" )
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
 | "Print" "Namespace" dirpath
 | "Inspect" num
 | "Add" "ML" "Path" string
 | "Add" "Rec" "ML" "Path" string
-| "Set" ident_list option_setting
-| "Unset" ident_list
-| "Print" "Table" ident_list
-| "Add" ident ident option_ref_value_list
-| "Add" ident option_ref_value_list
-| "Test" ident_list "for" option_ref_value_list
-| "Test" ident_list
-| "Remove" ident ident option_ref_value_list
-| "Remove" ident option_ref_value_list
+| "Set" LIST1 ident option_setting
+| "Unset" LIST1 ident
+| "Print" "Table" LIST1 ident
+| "Add" ident ident LIST1 option_ref_value
+| "Add" ident LIST1 option_ref_value
+| "Test" LIST1 ident "for" LIST1 option_ref_value
+| "Test" LIST1 ident
+| "Remove" ident ident LIST1 option_ref_value
+| "Remove" ident LIST1 option_ref_value
 | "Write" "State" ident
 | "Write" "State" string
 | "Restore" "State" ident
@@ -1328,9 +873,11 @@ command: [
 | "Show" "Intros"
 | "Show" "Match" qualid
 | "Guarded"
-| "Create" "HintDb" ident discriminated_opt
-| "Remove" "Hints" qualid_list opt_hintbases
+| "Create" "HintDb" ident [ "discriminated" | ]
+| "Remove" "Hints" LIST1 qualid opt_hintbases
 | "Hint" hint opt_hintbases
+| "Comments" LIST0 comment
+| "Declare" "Instance" ident_decl LIST0 binder ":" term hint_info
 | "Obligation" int "of" ident ":" term withtac
 | "Obligation" int "of" ident withtac
 | "Obligation" int ":" term withtac
@@ -1360,20 +907,20 @@ command: [
 | "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
 | "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
 | "Add" "Relation" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "as" ident
-| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
-| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
+| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
 | "Add" "Setoid" term1_extended term1_extended term1_extended "as" ident
-| "Add" "Parametric" "Setoid" binders_opt ":" term1_extended term1_extended term1_extended "as" ident
+| "Add" "Parametric" "Setoid" LIST0 binder ":" term1_extended term1_extended term1_extended "as" ident
 | "Add" "Morphism" term1_extended ":" ident
 | "Declare" "Morphism" term1_extended ":" ident
 | "Add" "Morphism" term1_extended "with" "signature" term "as" ident
-| "Add" "Parametric" "Morphism" binders_opt ":" term1_extended "with" "signature" term "as" ident
+| "Add" "Parametric" "Morphism" LIST0 binder ":" term1_extended "with" "signature" term "as" ident
 | "Grab" "Existential" "Variables"
 | "Unshelve"
 | "Declare" "Equivalent" "Keys" term1_extended term1_extended
@@ -1401,49 +948,49 @@ command: [
 | "Show" "Zify" "CstOp"      (* micromega plugin *)
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
 | "Show" "Zify" "Spec"      (* micromega plugin *)
-| "Add" "Ring" ident ":" term1_extended ring_mods_opt      (* setoid_ring plugin *)
+| "Add" "Ring" ident ":" term1_extended OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* setoid_ring plugin *)
 | "Hint" "Cut" "[" hints_path "]" opthints
-| "Typeclasses" "Transparent" qualid_list_opt
-| "Typeclasses" "Opaque" qualid_list_opt
-| "Typeclasses" "eauto" ":=" debug eauto_search_strategy int_opt
+| "Typeclasses" "Transparent" LIST0 qualid
+| "Typeclasses" "Opaque" LIST0 qualid
+| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int
+| "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
+| "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
+| "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
-| "Proof" "with" ltac_expr using_opt
-| "Proof" "using" section_subset_expr with_opt
-| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" ltac_expr
 | "Print" "Ltac" qualid
 | "Locate" "Ltac" qualid
-| "Ltac" tacdef_body_list
+| "Ltac" LIST1 tacdef_body SEP "with"
 | "Print" "Ltac" "Signatures"
 | "Set" "Firstorder" "Solver" ltac_expr
 | "Print" "Firstorder" "Solver"
+| "Function" LIST1 fix_definition SEP "with"      (* funind plugin *)
+| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
 | "Extraction" qualid      (* extraction plugin *)
-| "Recursive" "Extraction" qualid_list      (* extraction plugin *)
-| "Extraction" string qualid_list      (* extraction plugin *)
-| "Extraction" "TestCompile" qualid_list      (* extraction plugin *)
-| "Separate" "Extraction" qualid_list      (* extraction plugin *)
+| "Recursive" "Extraction" LIST1 qualid      (* extraction plugin *)
+| "Extraction" string LIST1 qualid      (* extraction plugin *)
+| "Extraction" "TestCompile" LIST1 qualid      (* extraction plugin *)
+| "Separate" "Extraction" LIST1 qualid      (* extraction plugin *)
 | "Extraction" "Library" ident      (* extraction plugin *)
 | "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
 | "Extraction" "Language" language      (* extraction plugin *)
-| "Extraction" "Inline" qualid_list      (* extraction plugin *)
-| "Extraction" "NoInline" qualid_list      (* extraction plugin *)
+| "Extraction" "Inline" LIST1 qualid      (* extraction plugin *)
+| "Extraction" "NoInline" LIST1 qualid      (* extraction plugin *)
 | "Print" "Extraction" "Inline"      (* extraction plugin *)
 | "Reset" "Extraction" "Inline"      (* extraction plugin *)
-| "Extraction" "Implicit" qualid "[" int_or_id_list_opt "]"      (* extraction plugin *)
-| "Extraction" "Blacklist" ident_list      (* extraction plugin *)
+| "Extraction" "Implicit" qualid "[" LIST0 int_or_id "]"      (* extraction plugin *)
+| "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
 | "Print" "Extraction" "Blacklist"      (* extraction plugin *)
 | "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
-| "Extract" "Constant" qualid string_list_opt "=>" mlname      (* extraction plugin *)
+| "Extract" "Constant" qualid LIST0 string "=>" mlname      (* extraction plugin *)
 | "Extract" "Inlined" "Constant" qualid "=>" mlname      (* extraction plugin *)
-| "Extract" "Inductive" qualid "=>" mlname "[" mlname_list_opt "]" string_opt      (* extraction plugin *)
+| "Extract" "Inductive" qualid "=>" mlname "[" LIST0 mlname "]" OPT string      (* extraction plugin *)
 | "Show" "Extraction"      (* extraction plugin *)
-| "Function" fix_definition_list      (* funind plugin *)
-| "Functional" "Scheme" fun_scheme_arg_list      (* funind plugin *)
 | "Functional" "Case" fun_scheme_arg      (* funind plugin *)
 | "Generate" "graph" "for" qualid      (* funind plugin *)
-| "Hint" "Rewrite" orient term1_extended_list ":" ident_list_opt
-| "Hint" "Rewrite" orient term1_extended_list "using" ltac_expr ":" ident_list_opt
-| "Hint" "Rewrite" orient term1_extended_list
-| "Hint" "Rewrite" orient term1_extended_list "using" ltac_expr
+| "Hint" "Rewrite" orient LIST1 term1_extended ":" LIST0 ident
+| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr ":" LIST0 ident
+| "Hint" "Rewrite" orient LIST1 term1_extended
+| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr
 | "Derive" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
 | "Derive" "Inversion_clear" ident "with" term1_extended
 | "Derive" "Inversion" ident "with" term1_extended "Sort" sort_family
@@ -1453,7 +1000,7 @@ command: [
 | "Declare" "Left" "Step" term1_extended
 | "Declare" "Right" "Step" term1_extended
 | "Print" "Rings"      (* setoid_ring plugin *)
-| "Add" "Field" ident ":" term1_extended field_mods_opt      (* setoid_ring plugin *)
+| "Add" "Field" ident ":" term1_extended OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
 | "Numeral" "Notation" qualid qualid qualid ":" ident numnotoption
 | "String" "Notation" qualid qualid qualid ":" ident
@@ -1462,31 +1009,11 @@ command: [
 orient: [
 | "->"
 | "<-"
-| empty
-]
-
-string_opt: [
-| string
-| empty
-]
-
-qualid_list_opt: [
-| qualid_list_opt qualid
-| empty
-]
-
-univ_name_list_opt: [
-| "@{" name_list_opt "}"
-| empty
-]
-
-name_list_opt: [
-| name_list_opt name
-| empty
+|
 ]
 
 section_subset_expr: [
-| starredidentref_list_opt
+| LIST0 starredidentref
 | ssexpr
 ]
 
@@ -1503,17 +1030,12 @@ ssexpr50: [
 
 ssexpr0: [
 | starredidentref
-| "(" starredidentref_list_opt ")"
-| "(" starredidentref_list_opt ")" "*"
+| "(" LIST0 starredidentref ")"
+| "(" LIST0 starredidentref ")" "*"
 | "(" ssexpr ")"
 | "(" ssexpr ")" "*"
 ]
 
-starredidentref_list_opt: [
-| starredidentref_list_opt starredidentref
-| empty
-]
-
 starredidentref: [
 | ident
 | ident "*"
@@ -1521,43 +1043,13 @@ starredidentref: [
 | "Type" "*"
 ]
 
-int_opt: [
-| int
-| empty
-]
-
-using_opt: [
-| "using" section_subset_expr
-| empty
-]
-
-with_opt: [
-| "with" ltac_expr
-| empty
-]
-
-ltac_tactic_level_opt: [
-| "(" "at" "level" num ")"
-| empty
-]
-
-ltac_production_item_list: [
-| ltac_production_item_list ltac_production_item
-| ltac_production_item
-]
-
-tacdef_body_list: [
-| tacdef_body_list "with" tacdef_body
-| tacdef_body
-]
-
 printable: [
-| "Term" smart_global univ_name_list_opt
+| "Term" smart_global OPT ( "@{" LIST0 name "}" )
 | "All"
 | "Section" qualid
 | "Grammar" ident
 | "Custom" "Grammar" ident
-| "LoadPath" dirpath_opt
+| "LoadPath" OPT dirpath
 | "Modules"
 | "Libraries"
 | "ML" "Path"
@@ -1579,9 +1071,9 @@ printable: [
 | "HintDb" ident
 | "Scopes"
 | "Scope" ident
-| "Visibility" ident_opt
+| "Visibility" OPT ident
 | "Implicit" smart_global
-| Sorted_opt "Universes" printunivs_subgraph_opt string_opt
+| [ "Sorted" | ] "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
 | "Assumptions" smart_global
 | "Opaque" "Dependencies" smart_global
 | "Transparent" "Dependencies" smart_global
@@ -1591,84 +1083,9 @@ printable: [
 | "Registered"
 ]
 
-dirpath_opt: [
-| dirpath
-| empty
-]
-
 dirpath: [
 | ident
-| dirpath field
-]
-
-Sorted_opt: [
-| "Sorted"
-| empty
-]
-
-printunivs_subgraph_opt: [
-| "Subgraph" "(" qualid_list_opt ")"
-| empty
-]
-
-comment_list_opt: [
-| comment_list_opt comment
-| empty
-]
-
-Verbose_opt: [
-| "Verbose"
-| empty
-]
-
-string_alt: [
-| string
-| ident
-]
-
-string_list: [
-| string_list string
-| string
-]
-
-option_ref_value_list: [
-| option_ref_value_list option_ref_value
-| option_ref_value
-]
-
-discriminated_opt: [
-| "discriminated"
-| empty
-]
-
-string_list_opt: [
-| string_list_opt string
-| empty
-]
-
-mlname_list_opt: [
-| mlname_list_opt mlname
-| empty
-]
-
-fun_scheme_arg_list: [
-| fun_scheme_arg_list "with" fun_scheme_arg
-| fun_scheme_arg
-]
-
-term1_extended_list: [
-| term1_extended_list term1_extended
-| term1_extended
-]
-
-ring_mods_opt: [
-| "(" ring_mod_list_comma ")"      (* setoid_ring plugin *)
-| empty
-]
-
-field_mods_opt: [
-| "(" field_mod_list_comma ")"      (* setoid_ring plugin *)
-| empty
+| dirpath field_ident
 ]
 
 locatable: [
@@ -1685,8 +1102,7 @@ option_ref_value: [
 ]
 
 as_dirpath: [
-| "as" dirpath
-| empty
+| OPT [ "as" dirpath ]
 ]
 
 comment: [
@@ -1701,25 +1117,20 @@ reference_or_constr: [
 ]
 
 hint: [
-| "Resolve" reference_or_constr_list hint_info
-| "Resolve" "->" qualid_list num_opt
-| "Resolve" "<-" qualid_list num_opt
-| "Immediate" reference_or_constr_list
+| "Resolve" LIST1 reference_or_constr hint_info
+| "Resolve" "->" LIST1 qualid OPT num
+| "Resolve" "<-" LIST1 qualid OPT num
+| "Immediate" LIST1 reference_or_constr
 | "Variables" "Transparent"
 | "Variables" "Opaque"
 | "Constants" "Transparent"
 | "Constants" "Opaque"
-| "Transparent" qualid_list
-| "Opaque" qualid_list
-| "Mode" qualid plus_list
-| "Unfold" qualid_list
-| "Constructors" qualid_list
-| "Extern" num term1_extended_opt "=>" ltac_expr
-]
-
-reference_or_constr_list: [
-| reference_or_constr_list reference_or_constr
-| reference_or_constr
+| "Transparent" LIST1 qualid
+| "Opaque" LIST1 qualid
+| "Mode" qualid LIST1 [ "+" | "!" | "-" ]
+| "Unfold" LIST1 qualid
+| "Constructors" LIST1 qualid
+| "Extern" num OPT term1_extended "=>" ltac_expr
 ]
 
 constr_body: [
@@ -1727,20 +1138,9 @@ constr_body: [
 | ":" term ":=" term
 ]
 
-plus_list: [
-| plus_list plus_alt
-| plus_alt
-]
-
-plus_alt: [
-| "+"
-| "!"
-| "-"
-]
-
 withtac: [
 | "with" ltac_expr
-| empty
+|
 ]
 
 ltac_def_kind: [
@@ -1749,23 +1149,18 @@ ltac_def_kind: [
 ]
 
 tacdef_body: [
-| qualid fun_var_list ltac_def_kind ltac_expr
+| qualid LIST1 fun_var ltac_def_kind ltac_expr
 | qualid ltac_def_kind ltac_expr
 ]
 
 ltac_production_item: [
 | string
-| ident "(" ident ltac_production_sep_opt ")"
+| ident "(" ident OPT ( "," string ) ")"
 | ident
 ]
 
-ltac_production_sep_opt: [
-| "," string
-| empty
-]
-
 numnotoption: [
-| empty
+|
 | "(" "warning" "after" num ")"
 | "(" "abstract" "after" num ")"
 ]
@@ -1797,44 +1192,34 @@ ring_mod: [
 | "abstract"      (* setoid_ring plugin *)
 | "morphism" term1_extended      (* setoid_ring plugin *)
 | "constants" "[" ltac_expr "]"      (* setoid_ring plugin *)
-| "closed" "[" qualid_list "]"      (* setoid_ring plugin *)
+| "closed" "[" LIST1 qualid "]"      (* setoid_ring plugin *)
 | "preprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
 | "postprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
 | "setoid" term1_extended term1_extended      (* setoid_ring plugin *)
 | "sign" term1_extended      (* setoid_ring plugin *)
-| "power" term1_extended "[" qualid_list "]"      (* setoid_ring plugin *)
+| "power" term1_extended "[" LIST1 qualid "]"      (* setoid_ring plugin *)
 | "power_tac" term1_extended "[" ltac_expr "]"      (* setoid_ring plugin *)
 | "div" term1_extended      (* setoid_ring plugin *)
 ]
 
-ring_mod_list_comma: [
-| ring_mod_list_comma "," ring_mod
-| ring_mod
-]
-
 field_mod: [
 | ring_mod      (* setoid_ring plugin *)
 | "completeness" term1_extended      (* setoid_ring plugin *)
 ]
 
-field_mod_list_comma: [
-| field_mod_list_comma "," field_mod
-| field_mod
-]
-
 debug: [
 | "debug"
-| empty
+|
 ]
 
 eauto_search_strategy: [
 | "(bfs)"
 | "(dfs)"
-| empty
+|
 ]
 
 hints_path_atom: [
-| qualid_list
+| LIST1 qualid
 | "_"
 ]
 
@@ -1849,62 +1234,52 @@ hints_path: [
 ]
 
 opthints: [
-| ":" ident_list
-| empty
+| ":" LIST1 ident
+|
 ]
 
 opt_hintbases: [
-| empty
-| ":" ident_list
-]
-
-int_or_id_list_opt: [
-| int_or_id_list_opt int_or_id
-| empty
+|
+| ":" LIST1 ident
 ]
 
 query_command: [
 | "Eval" red_expr "in" term "."
 | "Compute" term "."
 | "Check" term "."
-| "About" smart_global univ_name_list_opt "."
+| "About" smart_global OPT ( "@{" LIST0 name "}" ) "."
 | "SearchHead" term1_extended in_or_out_modules "."
 | "SearchPattern" term1_extended in_or_out_modules "."
 | "SearchRewrite" term1_extended in_or_out_modules "."
 | "Search" searchabout_query searchabout_queries "."
 | "SearchAbout" searchabout_query searchabout_queries "."
-| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "."
+| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
 ]
 
 ne_in_or_out_modules: [
-| "inside" qualid_list
-| "outside" qualid_list
+| "inside" LIST1 qualid
+| "outside" LIST1 qualid
 ]
 
 in_or_out_modules: [
 | ne_in_or_out_modules
-| empty
+|
 ]
 
 positive_search_mark: [
 | "-"
-| empty
+|
 ]
 
 searchabout_query: [
-| positive_search_mark string scope_delimiter_opt
+| positive_search_mark string OPT ( "%" ident )
 | positive_search_mark term1_extended
 ]
 
 searchabout_queries: [
 | ne_in_or_out_modules
 | searchabout_query searchabout_queries
-| empty
-]
-
-searchabout_query_list: [
-| searchabout_query_list searchabout_query
-| searchabout_query
+|
 ]
 
 syntax: [
@@ -1912,34 +1287,18 @@ syntax: [
 | "Close" "Scope" ident
 | "Delimit" "Scope" ident "with" ident
 | "Undelimit" "Scope" ident
-| "Bind" "Scope" ident "with" class_rawexpr_list
-| "Infix" string ":=" term1_extended syntax_modifier_opt ident_opt3
-| "Notation" ident ident_list_opt ":=" term1_extended only_parsing
-| "Notation" string ":=" term1_extended syntax_modifier_opt ident_opt3
+| "Bind" "Scope" ident "with" LIST1 class_rawexpr
+| "Infix" string ":=" term1_extended [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" ident ]
+| "Notation" ident LIST0 ident ":=" term1_extended only_parsing
+| "Notation" string ":=" term1_extended [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" ident ]
 | "Format" "Notation" string string string
-| "Reserved" "Infix" string syntax_modifier_opt
-| "Reserved" "Notation" string syntax_modifier_opt
-]
-
-class_rawexpr_list: [
-| class_rawexpr_list class_rawexpr
-| class_rawexpr
-]
-
-syntax_modifier_opt: [
-| "(" syntax_modifier_list_comma ")"
-| empty
-]
-
-syntax_modifier_list_comma: [
-| syntax_modifier_list_comma "," syntax_modifier
-| syntax_modifier
+| "Reserved" "Infix" string [ "(" LIST1 syntax_modifier SEP "," ")" | ]
+| "Reserved" "Notation" string [ "(" LIST1 syntax_modifier SEP "," ")" | ]
 ]
 
 only_parsing: [
 | "(" "only" "parsing" ")"
-| "(" "compat" string ")"
-| empty
+|
 ]
 
 level: [
@@ -1956,9 +1315,8 @@ syntax_modifier: [
 | "no" "associativity"
 | "only" "printing"
 | "only" "parsing"
-| "compat" string
-| "format" string string_opt
-| ident "," ident_list_comma "at" level
+| "format" string OPT string
+| ident "," LIST1 ident SEP "," "at" level
 | ident "at" level
 | ident "at" level constr_as_binder_kind
 | ident constr_as_binder_kind
@@ -1971,23 +1329,13 @@ syntax_extension_type: [
 | "bigint"
 | "binder"
 | "constr"
-| "constr" level_opt constr_as_binder_kind_opt
+| "constr" OPT ( "at" level ) OPT constr_as_binder_kind
 | "pattern"
 | "pattern" "at" "level" num
 | "strict" "pattern"
 | "strict" "pattern" "at" "level" num
 | "closed" "binder"
-| "custom" ident level_opt constr_as_binder_kind_opt
-]
-
-level_opt: [
-| level
-| empty
-]
-
-constr_as_binder_kind_opt: [
-| constr_as_binder_kind
-| empty
+| "custom" ident OPT ( "at" level ) OPT constr_as_binder_kind
 ]
 
 constr_as_binder_kind: [
@@ -2032,9 +1380,9 @@ simple_tactic: [
 | "split" "with" bindings
 | "esplit" "with" bindings
 | "exists"
-| "exists" bindings_list_comma
+| "exists" LIST1 bindings SEP ","
 | "eexists"
-| "eexists" bindings_list_comma
+| "eexists" LIST1 bindings SEP ","
 | "intros" "until" quantified_hypothesis
 | "intro"
 | "intro" ident
@@ -2050,17 +1398,17 @@ simple_tactic: [
 | "move" ident "at" "bottom"
 | "move" ident "after" ident
 | "move" ident "before" ident
-| "rename" rename_list_comma
-| "revert" ident_list
+| "rename" LIST1 rename SEP ","
+| "revert" LIST1 ident
 | "simple" "induction" quantified_hypothesis
 | "simple" "destruct" quantified_hypothesis
 | "double" "induction" quantified_hypothesis quantified_hypothesis
 | "admit"
 | "fix" ident num
 | "cofix" ident
-| "clear" ident_list_opt
-| "clear" "-" ident_list
-| "clearbody" ident_list
+| "clear" LIST0 ident
+| "clear" "-" LIST1 ident
+| "clearbody" LIST1 ident
 | "generalize" "dependent" term1_extended
 | "replace" term1_extended "with" term1_extended clause_dft_concl by_arg_tac
 | "replace" "->" term1_extended clause_dft_concl
@@ -2078,10 +1426,10 @@ simple_tactic: [
 | "injection" destruction_arg
 | "einjection"
 | "einjection" destruction_arg
-| "injection" "as" simple_intropattern_list_opt
-| "injection" destruction_arg "as" simple_intropattern_list_opt
-| "einjection" "as" simple_intropattern_list_opt
-| "einjection" destruction_arg "as" simple_intropattern_list_opt
+| "injection" "as" LIST0 simple_intropattern
+| "injection" destruction_arg "as" LIST0 simple_intropattern
+| "einjection" "as" LIST0 simple_intropattern
+| "einjection" destruction_arg "as" LIST0 simple_intropattern
 | "simple" "injection"
 | "simple" "injection" destruction_arg
 | "dependent" "rewrite" orient term1_extended
@@ -2091,11 +1439,11 @@ simple_tactic: [
 | "decompose" "sum" term1_extended
 | "decompose" "record" term1_extended
 | "absurd" term1_extended
-| "contradiction" constr_with_bindings_opt
-| "autorewrite" "with" ident_list clause_dft_concl
-| "autorewrite" "with" ident_list clause_dft_concl "using" ltac_expr
-| "autorewrite" "*" "with" ident_list clause_dft_concl
-| "autorewrite" "*" "with" ident_list clause_dft_concl "using" ltac_expr
+| "contradiction" OPT constr_with_bindings
+| "autorewrite" "with" LIST1 ident clause_dft_concl
+| "autorewrite" "with" LIST1 ident clause_dft_concl "using" ltac_expr
+| "autorewrite" "*" "with" LIST1 ident clause_dft_concl
+| "autorewrite" "*" "with" LIST1 ident clause_dft_concl "using" ltac_expr
 | "rewrite" "*" orient term1_extended "in" ident "at" occurrences by_arg_tac
 | "rewrite" "*" orient term1_extended "at" occurrences "in" ident by_arg_tac
 | "rewrite" "*" orient term1_extended "in" ident by_arg_tac
@@ -2106,7 +1454,7 @@ simple_tactic: [
 | "notypeclasses" "refine" term1_extended
 | "simple" "notypeclasses" "refine" term1_extended
 | "solve_constraints"
-| "subst" ident_list
+| "subst" LIST1 ident
 | "subst"
 | "simple" "subst"
 | "evar" "(" ident ":" term ")"
@@ -2150,7 +1498,7 @@ simple_tactic: [
 | "swap" int_or_var int_or_var
 | "revgoals"
 | "guard" int_or_var comparison int_or_var
-| "decompose" "[" term1_extended_list "]" term1_extended
+| "decompose" "[" LIST1 term1_extended "]" term1_extended
 | "optimize_heap"
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
@@ -2158,32 +1506,32 @@ simple_tactic: [
 | "show" "ltac" "profile"
 | "show" "ltac" "profile" "cutoff" int
 | "show" "ltac" "profile" string
-| "restart_timer" string_opt
-| "finish_timing" string_opt
-| "finish_timing" "(" string ")" string_opt
+| "restart_timer" OPT string
+| "finish_timing" OPT string
+| "finish_timing" "(" string ")" OPT string
 | "eassumption"
 | "eexact" term1_extended
 | "trivial" auto_using hintbases
 | "info_trivial" auto_using hintbases
 | "debug" "trivial" auto_using hintbases
-| "auto" int_or_var_opt auto_using hintbases
-| "info_auto" int_or_var_opt auto_using hintbases
-| "debug" "auto" int_or_var_opt auto_using hintbases
-| "prolog" "[" term1_extended_list_opt "]" int_or_var
-| "eauto" int_or_var_opt int_or_var_opt auto_using hintbases
-| "new" "auto" int_or_var_opt auto_using hintbases
-| "debug" "eauto" int_or_var_opt int_or_var_opt auto_using hintbases
-| "info_eauto" int_or_var_opt int_or_var_opt auto_using hintbases
-| "dfs" "eauto" int_or_var_opt auto_using hintbases
+| "auto" OPT int_or_var auto_using hintbases
+| "info_auto" OPT int_or_var auto_using hintbases
+| "debug" "auto" OPT int_or_var auto_using hintbases
+| "prolog" "[" LIST0 term1_extended "]" int_or_var
+| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
+| "new" "auto" OPT int_or_var auto_using hintbases
+| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
+| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases
+| "dfs" "eauto" OPT int_or_var auto_using hintbases
 | "autounfold" hintbases clause_dft_concl
 | "autounfold_one" hintbases "in" ident
 | "autounfold_one" hintbases
 | "unify" term1_extended term1_extended
 | "unify" term1_extended term1_extended "with" ident
 | "convert_concl_no_check" term1_extended
-| "typeclasses" "eauto" "bfs" int_or_var_opt "with" ident_list
-| "typeclasses" "eauto" int_or_var_opt "with" ident_list
-| "typeclasses" "eauto" int_or_var_opt
+| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 ident
+| "typeclasses" "eauto" OPT int_or_var "with" LIST1 ident
+| "typeclasses" "eauto" OPT int_or_var
 | "head_of_constr" ident term1_extended
 | "not_evar" term1_extended
 | "is_ground" term1_extended
@@ -2209,16 +1557,16 @@ simple_tactic: [
 | "rewrite_strat" rewstrategy "in" ident
 | "intros" intropattern_list_opt
 | "eintros" intropattern_list_opt
-| "apply" constr_with_bindings_arg_list_comma in_hyp_as
-| "eapply" constr_with_bindings_arg_list_comma in_hyp_as
-| "simple" "apply" constr_with_bindings_arg_list_comma in_hyp_as
-| "simple" "eapply" constr_with_bindings_arg_list_comma in_hyp_as
-| "elim" constr_with_bindings_arg eliminator_opt
-| "eelim" constr_with_bindings_arg eliminator_opt
+| "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
+| "elim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
+| "eelim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
 | "case" induction_clause_list
 | "ecase" induction_clause_list
-| "fix" ident num "with" fixdecl_list
-| "cofix" ident "with" cofixdecl_list
+| "fix" ident num "with" LIST1 fixdecl
+| "cofix" ident "with" LIST1 cofixdecl
 | "pose" bindings_with_parameters
 | "pose" term1_extended as_name
 | "epose" bindings_with_parameters
@@ -2242,47 +1590,47 @@ simple_tactic: [
 | "enough" term1_extended as_ipat by_tactic
 | "eenough" term1_extended as_ipat by_tactic
 | "generalize" term1_extended
-| "generalize" term1_extended term1_extended_list
-| "generalize" term1_extended occs as_name pattern_occ_list_opt
+| "generalize" term1_extended LIST1 term1_extended
+| "generalize" term1_extended occs as_name LIST0 [ "," pattern_occ as_name ]
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
 | "edestruct" induction_clause_list
-| "rewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic
-| "erewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic
-| "dependent" simple_alt quantified_hypothesis as_or_and_ipat with_opt2
+| "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
+| "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
+| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" term1_extended ]
 | "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
 | "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
 | "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list
 | "inversion" quantified_hypothesis "using" term1_extended in_hyp_list
 | "red" clause_dft_concl
 | "hnf" clause_dft_concl
-| "simpl" delta_flag ref_or_pattern_occ_opt clause_dft_concl
+| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl
 | "cbv" strategy_flag clause_dft_concl
 | "cbn" strategy_flag clause_dft_concl
 | "lazy" strategy_flag clause_dft_concl
 | "compute" delta_flag clause_dft_concl
-| "vm_compute" ref_or_pattern_occ_opt clause_dft_concl
-| "native_compute" ref_or_pattern_occ_opt clause_dft_concl
-| "unfold" unfold_occ_list_comma clause_dft_concl
-| "fold" term1_extended_list clause_dft_concl
-| "pattern" pattern_occ_list_comma clause_dft_concl
+| "vm_compute" OPT ref_or_pattern_occ clause_dft_concl
+| "native_compute" OPT ref_or_pattern_occ clause_dft_concl
+| "unfold" LIST1 unfold_occ SEP "," clause_dft_concl
+| "fold" LIST1 term1_extended clause_dft_concl
+| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl
 | "change" conversion clause_dft_concl
 | "change_no_check" conversion clause_dft_concl
 | "btauto"
 | "rtauto"
 | "congruence"
 | "congruence" int
-| "congruence" "with" term1_extended_list
-| "congruence" int "with" term1_extended_list
+| "congruence" "with" LIST1 term1_extended
+| "congruence" int "with" LIST1 term1_extended
 | "f_equal"
-| "firstorder" ltac_expr_opt firstorder_using
-| "firstorder" ltac_expr_opt "with" ident_list
-| "firstorder" ltac_expr_opt firstorder_using "with" ident_list
-| "gintuition" ltac_expr_opt
-| "functional" "inversion" quantified_hypothesis qualid_opt      (* funind plugin *)
-| "functional" "induction" term1_extended_list fun_ind_using with_names      (* funind plugin *)
-| "soft" "functional" "induction" term1_extended_list fun_ind_using with_names      (* funind plugin *)
+| "firstorder" OPT ltac_expr firstorder_using
+| "firstorder" OPT ltac_expr "with" LIST1 ident
+| "firstorder" OPT ltac_expr firstorder_using "with" LIST1 ident
+| "gintuition" OPT ltac_expr
+| "functional" "inversion" quantified_hypothesis OPT qualid      (* funind plugin *)
+| "functional" "induction" LIST1 term1_extended fun_ind_using with_names      (* funind plugin *)
+| "soft" "functional" "induction" LIST1 term1_extended fun_ind_using with_names      (* funind plugin *)
 | "myred"      (* micromega plugin *)
 | "psatz_Z" int_or_var ltac_expr      (* micromega plugin *)
 | "psatz_Z" ltac_expr      (* micromega plugin *)
@@ -2304,12 +1652,12 @@ simple_tactic: [
 | "saturate"      (* micromega plugin *)
 | "nsatz_compute" term1_extended      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
-| "omega" "with" ident_list      (* omega plugin *)
+| "omega" "with" LIST1 ident      (* omega plugin *)
 | "omega" "with" "*"      (* omega plugin *)
 | "protect_fv" string "in" ident      (* setoid_ring plugin *)
 | "protect_fv" string      (* setoid_ring plugin *)
-| "ring_lookup" ltac_expr0 "[" term1_extended_list_opt "]" term1_extended_list      (* setoid_ring plugin *)
-| "field_lookup" ltac_expr "[" term1_extended_list_opt "]" term1_extended_list      (* setoid_ring plugin *)
+| "ring_lookup" ltac_expr0 "[" LIST0 term1_extended "]" LIST1 term1_extended      (* setoid_ring plugin *)
+| "field_lookup" ltac_expr "[" LIST0 term1_extended "]" LIST1 term1_extended      (* setoid_ring plugin *)
 ]
 
 int_or_var: [
@@ -2317,13 +1665,8 @@ int_or_var: [
 | ident
 ]
 
-constr_with_bindings_opt: [
-| constr_with_bindings
-| empty
-]
-
 hloc: [
-| empty
+|
 | "in" "|-" "*"
 | "in" ident
 | "in" "(" "Type" "of" ident ")"
@@ -2338,30 +1681,25 @@ rename: [
 
 by_arg_tac: [
 | "by" ltac_expr3
-| empty
+|
 ]
 
 in_clause: [
 | in_clause
 | "*" occs
 | "*" "|-" concl_occ
-| hypident_occ_list_comma_opt "|-" concl_occ
-| hypident_occ_list_comma_opt
+| LIST0 hypident_occ SEP "," "|-" concl_occ
+| LIST0 hypident_occ SEP ","
 ]
 
 occs: [
 | "at" occs_nums
-| empty
-]
-
-hypident_occ_list_comma_opt: [
-| hypident_occ_list_comma
-| empty
+|
 ]
 
 as_ipat: [
 | "as" simple_intropattern
-| empty
+|
 ]
 
 or_and_intropattern_loc: [
@@ -2371,40 +1709,35 @@ or_and_intropattern_loc: [
 
 as_or_and_ipat: [
 | "as" or_and_intropattern_loc
-| empty
+|
 ]
 
 eqn_ipat: [
 | "eqn" ":" naming_intropattern
 | "_eqn" ":" naming_intropattern
 | "_eqn"
-| empty
+|
 ]
 
 as_name: [
 | "as" ident
-| empty
+|
 ]
 
 by_tactic: [
 | "by" ltac_expr3
-| empty
+|
 ]
 
 rewriter: [
 | "!" constr_with_bindings_arg
-| qmark_alt constr_with_bindings_arg
+| [ "?" | "?" ] constr_with_bindings_arg
 | num "!" constr_with_bindings_arg
-| num qmark_alt constr_with_bindings_arg
+| num [ "?" | "?" ] constr_with_bindings_arg
 | num constr_with_bindings_arg
 | constr_with_bindings_arg
 ]
 
-qmark_alt: [
-| "?"
-| "?"
-]
-
 oriented_rewriter: [
 | orient rewriter
 ]
@@ -2414,53 +1747,22 @@ induction_clause: [
 ]
 
 induction_clause_list: [
-| induction_clause_list_comma eliminator_opt opt_clause
-]
-
-induction_clause_list_comma: [
-| induction_clause_list_comma "," induction_clause
-| induction_clause
-]
-
-eliminator_opt: [
-| "using" constr_with_bindings
-| empty
+| LIST1 induction_clause SEP "," OPT ( "using" constr_with_bindings ) opt_clause
 ]
 
 auto_using: [
-| "using" term1_extended_list_comma
-| empty
-]
-
-term1_extended_list_comma: [
-| term1_extended_list_comma "," term1_extended
-| term1_extended
+| "using" LIST1 term1_extended SEP ","
+|
 ]
 
 intropattern_list_opt: [
-| intropattern_list_opt intropattern
-| empty
+| LIST0 intropattern
 ]
 
 or_and_intropattern: [
 | "[" intropattern_or_list_or "]"
-| "(" simple_intropattern_list_comma_opt ")"
-| "(" simple_intropattern "&" simple_intropattern_list_ ")"
-]
-
-simple_intropattern_list_comma_opt: [
-| simple_intropattern_list_comma
-| empty
-]
-
-simple_intropattern_list_comma: [
-| simple_intropattern_list_comma "," simple_intropattern
-| simple_intropattern
-]
-
-simple_intropattern_list_: [
-| simple_intropattern_list_ "&" simple_intropattern
-| simple_intropattern
+| "(" LIST0 simple_intropattern SEP "," ")"
+| "(" simple_intropattern "&" LIST1 simple_intropattern SEP "&" ")"
 ]
 
 intropattern_or_list_or: [
@@ -2468,11 +1770,6 @@ intropattern_or_list_or: [
 | intropattern_list_opt
 ]
 
-simple_intropattern_list_opt: [
-| simple_intropattern_list_opt simple_intropattern
-| empty
-]
-
 equality_intropattern: [
 | "->"
 | "<-"
@@ -2492,12 +1789,7 @@ intropattern: [
 ]
 
 simple_intropattern: [
-| simple_intropattern_closed term0_list_opt
-]
-
-term0_list_opt: [
-| term0_list_opt "%" term0
-| empty
+| simple_intropattern_closed LIST0 [ "%" term0 ]
 ]
 
 simple_intropattern_closed: [
@@ -2513,65 +1805,14 @@ simple_binding: [
 ]
 
 bindings: [
-| simple_binding_list
-| term1_extended_list
-]
-
-simple_binding_list: [
-| simple_binding_list simple_binding
-| simple_binding
-]
-
-constr_with_bindings_arg_list_comma: [
-| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg
-| constr_with_bindings_arg
-]
-
-fixdecl_list: [
-| fixdecl_list fixdecl
-| fixdecl
-]
-
-cofixdecl_list: [
-| cofixdecl_list cofixdecl
-| cofixdecl
-]
-
-pattern_occ_list_opt: [
-| pattern_occ_list_opt "," pattern_occ as_name
-| empty
+| LIST1 simple_binding
+| LIST1 term1_extended
 ]
 
 pattern_occ: [
 | term1_extended occs
 ]
 
-oriented_rewriter_list_comma: [
-| oriented_rewriter_list_comma "," oriented_rewriter
-| oriented_rewriter
-]
-
-simple_alt: [
-| "simple" "inversion"
-| "inversion"
-| "inversion_clear"
-]
-
-with_opt2: [
-| "with" term1_extended
-| empty
-]
-
-bindings_list_comma: [
-| bindings_list_comma "," bindings
-| bindings
-]
-
-rename_list_comma: [
-| rename_list_comma "," rename
-| rename
-]
-
 comparison: [
 | "="
 | "<"
@@ -2582,22 +1823,12 @@ comparison: [
 
 hintbases: [
 | "with" "*"
-| "with" ident_list
-| empty
-]
-
-qualid_opt: [
-| qualid
-| empty
+| "with" LIST1 ident
+|
 ]
 
 bindings_with_parameters: [
-| "(" ident simple_binder_list_opt ":=" term ")"
-]
-
-simple_binder_list_opt: [
-| simple_binder_list_opt simple_binder
-| empty
+| "(" ident LIST0 simple_binder ":=" term ")"
 ]
 
 hypident: [
@@ -2613,23 +1844,23 @@ hypident_occ: [
 clause_dft_concl: [
 | "in" in_clause
 | occs
-| empty
+|
 ]
 
 clause_dft_all: [
 | "in" in_clause
-| empty
+|
 ]
 
 opt_clause: [
 | "in" in_clause
 | "at" occs_nums
-| empty
+|
 ]
 
 occs_nums: [
-| num_or_var_list
-| "-" num_or_var int_or_var_list_opt
+| LIST1 num_or_var
+| "-" num_or_var LIST0 int_or_var
 ]
 
 num_or_var: [
@@ -2637,47 +1868,37 @@ num_or_var: [
 | ident
 ]
 
-int_or_var_list_opt: [
-| int_or_var_list_opt int_or_var
-| empty
-]
-
-num_or_var_list: [
-| num_or_var_list num_or_var
-| num_or_var
-]
-
 concl_occ: [
 | "*" occs
-| empty
+|
 ]
 
 in_hyp_list: [
-| "in" ident_list
-| empty
+| "in" LIST1 ident
+|
 ]
 
 in_hyp_as: [
 | "in" ident as_ipat
-| empty
+|
 ]
 
 simple_binder: [
 | name
-| "(" names ":" term ")"
+| "(" LIST1 name ":" term ")"
 ]
 
 fixdecl: [
-| "(" ident simple_binder_list_opt struct_annot ":" term ")"
+| "(" ident LIST0 simple_binder struct_annot ":" term ")"
 ]
 
 struct_annot: [
 | "{" "struct" name "}"
-| empty
+|
 ]
 
 cofixdecl: [
-| "(" ident simple_binder_list_opt ":" term ")"
+| "(" ident LIST0 simple_binder ":" term ")"
 ]
 
 constr_with_bindings: [
@@ -2686,7 +1907,7 @@ constr_with_bindings: [
 
 with_bindings: [
 | "with" bindings
-| empty
+|
 ]
 
 destruction_arg: [
@@ -2713,36 +1934,26 @@ conversion: [
 
 firstorder_using: [
 | "using" qualid
-| "using" qualid "," qualid_list_comma
-| "using" qualid qualid qualid_list_opt
-| empty
-]
-
-qualid_list_comma: [
-| qualid_list_comma "," qualid
-| qualid
+| "using" qualid "," LIST1 qualid SEP ","
+| "using" qualid qualid LIST0 qualid
+|
 ]
 
 fun_ind_using: [
 | "using" constr_with_bindings      (* funind plugin *)
-| empty      (* funind plugin *)
+|      (* funind plugin *)
 ]
 
 with_names: [
 | "as" simple_intropattern      (* funind plugin *)
-| empty      (* funind plugin *)
+|      (* funind plugin *)
 ]
 
 occurrences: [
-| int_list
+| LIST1 int
 | ident
 ]
 
-int_list: [
-| int_list int
-| int
-]
-
 rewstrategy: [
 | term1_extended
 | "<-" term1_extended
@@ -2764,51 +1975,31 @@ rewstrategy: [
 | "choice" rewstrategy rewstrategy
 | "old_hints" ident
 | "hints" ident
-| "terms" term1_extended_list_opt
+| "terms" LIST0 term1_extended
 | "eval" red_expr
 | "fold" term1_extended
 ]
 
-hypident_occ_list_comma: [
-| hypident_occ_list_comma "," hypident_occ
-| hypident_occ
-]
-
 ltac_expr: [
 | binder_tactic
 | ltac_expr4
 ]
 
 binder_tactic: [
-| "fun" fun_var_list "=>" ltac_expr
-| "let" rec_opt let_clause_list "in" ltac_expr
+| "fun" LIST1 fun_var "=>" ltac_expr
+| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr
 | "info" ltac_expr
 ]
 
-fun_var_list: [
-| fun_var_list fun_var
-| fun_var
-]
-
 fun_var: [
 | ident
 | "_"
 ]
 
-rec_opt: [
-| "rec"
-| empty
-]
-
-let_clause_list: [
-| let_clause_list "with" let_clause
-| let_clause
-]
-
 let_clause: [
 | ident ":=" ltac_expr
 | "_" ":=" ltac_expr
-| ident fun_var_list ":=" ltac_expr
+| ident LIST1 fun_var ":=" ltac_expr
 ]
 
 ltac_expr4: [
@@ -2820,27 +2011,28 @@ ltac_expr4: [
 ]
 
 multi_goal_tactics: [
-| ltac_expr_opt "|" multi_goal_tactics
-| ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
+| OPT ltac_expr "|" multi_goal_tactics
+| ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
 | ltac_expr
-| empty
+|
 ]
 
 ltac_expr_opt: [
-| ltac_expr
-| empty
+| OPT ltac_expr
 ]
 
 ltac_expr_opt_list_or: [
 | ltac_expr_opt_list_or "|" ltac_expr_opt
 | ltac_expr_opt
+| ltac_expr_opt_list_or "|" OPT ltac_expr
+| OPT ltac_expr
 ]
 
 ltac_expr3: [
 | "try" ltac_expr3
 | "do" int_or_var ltac_expr3
 | "timeout" int_or_var ltac_expr3
-| "time" string_opt ltac_expr3
+| "time" OPT string ltac_expr3
 | "repeat" ltac_expr3
 | "progress" ltac_expr3
 | "once" ltac_expr3
@@ -2863,48 +2055,23 @@ ltac_expr2: [
 
 ltac_expr1: [
 | ltac_match_term
+| "first" "[" LIST0 ltac_expr SEP "|" "]"
+| "solve" "[" LIST0 ltac_expr SEP "|" "]"
+| "idtac" LIST0 message_token
+| failkw [ int_or_var | ] LIST0 message_token
 | ltac_match_goal
-| "first" "[" ltac_expr_list_or_opt "]"
-| "solve" "[" ltac_expr_list_or_opt "]"
-| "idtac" message_token_list_opt
-| failkw int_or_var_opt message_token_list_opt
 | simple_tactic
 | tactic_arg
-| qualid tactic_arg_compat_list_opt
+| qualid LIST0 tactic_arg_compat
 | ltac_expr0
 ]
 
-ltac_expr_list_or_opt: [
-| ltac_expr_list_or
-| empty
-]
-
-ltac_expr_list_or: [
-| ltac_expr_list_or "|" ltac_expr
-| ltac_expr
-]
-
-message_token_list_opt: [
-| message_token_list_opt message_token
-| empty
-]
-
 message_token: [
 | ident
 | string
 | int
 ]
 
-int_or_var_opt: [
-| int_or_var
-| empty
-]
-
-term1_extended_list_opt: [
-| term1_extended_list_opt term1_extended
-| empty
-]
-
 failkw: [
 | "fail"
 | "gfail"
@@ -2914,26 +2081,16 @@ tactic_arg: [
 | "eval" red_expr "in" term
 | "context" ident "[" term "]"
 | "type" "of" term
-| "fresh" fresh_id_list_opt
+| "fresh" LIST0 fresh_id
 | "type_term" term1_extended
 | "numgoals"
 ]
 
-fresh_id_list_opt: [
-| fresh_id_list_opt fresh_id
-| empty
-]
-
 fresh_id: [
 | string
 | qualid
 ]
 
-tactic_arg_compat_list_opt: [
-| tactic_arg_compat_list_opt tactic_arg_compat
-| empty
-]
-
 tactic_arg_compat: [
 | tactic_arg
 | term
@@ -2963,22 +2120,17 @@ only_selector: [
 ]
 
 selector: [
-| range_selector_list_comma
+| LIST1 range_selector SEP ","
 | "[" ident "]"
 ]
 
-range_selector_list_comma: [
-| range_selector_list_comma "," range_selector
-| range_selector
-]
-
 range_selector: [
 | num "-" num
 | num
 ]
 
 ltac_match_term: [
-| match_key ltac_expr "with" or_opt match_rule_list_or "end"
+| match_key ltac_expr "with" OPT "|" LIST1 match_rule SEP "|" "end"
 ]
 
 match_key: [
@@ -2987,67 +2139,27 @@ match_key: [
 | "lazymatch"
 ]
 
-match_rule_list_or: [
-| match_rule_list_or "|" match_rule
-| match_rule
-]
-
 match_rule: [
-| match_pattern_alt "=>" ltac_expr
-]
-
-match_pattern_alt: [
-| match_pattern
-| "_"
+| [ match_pattern | "_" ] "=>" ltac_expr
 ]
 
 match_pattern: [
-| "context" ident_opt "[" term "]"
+| "context" OPT ident "[" term "]"
 | term
 ]
 
 ltac_match_goal: [
-| match_key reverse_opt "goal" "with" or_opt match_context_rule_list_or "end"
-]
-
-reverse_opt: [
-| "reverse"
-| empty
-]
-
-match_context_rule_list_or: [
-| match_context_rule_list_or "|" match_context_rule
-| match_context_rule
+| match_key OPT "reverse" "goal" "with" OPT "|" LIST1 match_context_rule SEP "|" "end"
 ]
 
 match_context_rule: [
-| match_hyp_list_comma_opt "|-" match_pattern "=>" ltac_expr
-| "[" match_hyp_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr
+| LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr
+| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr
 | "_" "=>" ltac_expr
 ]
 
-match_hyp_list_comma_opt: [
-| match_hyp_list_comma
-| empty
-]
-
-match_hyp_list_comma: [
-| match_hyp_list_comma "," match_hyp
-| match_hyp
-]
-
 match_hyp: [
 | name ":" match_pattern
-| name ":=" match_pattern_opt match_pattern
-]
-
-match_pattern_opt: [
-| "[" match_pattern "]" ":"
-| empty
-]
-
-ident_list_opt: [
-| ident_list_opt ident
-| empty
+| name ":=" OPT ( "[" match_pattern "]" ":" ) match_pattern
 ]
 
diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg
index 42d94e76bb..8170b71e7a 100644
--- a/doc/tools/docgram/productionlist.edit_mlg
+++ b/doc/tools/docgram/productionlist.edit_mlg
@@ -13,32 +13,6 @@
 
 DOC_GRAMMAR
 
-EXPAND: [ | ]
-
-RENAME: [
-| name_alt names_tuple
-| binder_list binders
-| binder_list_opt binders_opt
-| typeclass_constraint_list_comma typeclass_constraints_comma
-| universe_expr_list_comma universe_exprs_comma
-| universe_level_list_opt universe_levels_opt
-| name_list names
-| name_list_comma names_comma
-| case_item_list_comma case_items_comma
-| eqn_list_or_opt eqns_or_opt
-| eqn_list_or eqns_or
-| pattern_list_or patterns_or
-| fix_body_list fix_bodies
-| arg_list args
-| arg_list_opt args_opt
-| evar_binding_list_semi evar_bindings_semi
-]
-
-binders_opt: [
-| REPLACE binders_opt binder
-| WITH binders
-]
-
 (* this is here because they're inside _opt generated by EXPAND *)
 SPLICE: [
 | ltac_info