Convert Gallina Vernac to use prodn

6 files changed, 625 insertions, 413 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 8d74e3c1e5..d6ecf311f1 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -294,7 +294,7 @@ class VernacObject(NotationObject):
 
     Example::
 
-       .. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+       .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident }
 
           This command is equivalent to :n:`…`.
     """
@@ -346,7 +346,7 @@ class AttributeNotationObject(NotationObject):
 
     Example::
 
-       .. attr:: #[ local ]
+       .. attr:: local
     """
     subdomain = "attr"
     index_suffix = "(attribute)"
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 9c1827f5b7..3524d77380 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -39,7 +39,7 @@ RENAME: [
 | Prim.natural natural
 *)
 | Vernac.rec_definition rec_definition
-
+(* todo: hmm, rename adds 1 prodn to closed_binder?? *)
 | Constr.closed_binder closed_binder
 ]
 
@@ -162,11 +162,6 @@ lconstr: [
 | DELETE l_constr
 ]
 
-type_cstr: [
-| REPLACE ":" lconstr
-| WITH OPT ( ":" lconstr )
-| DELETE (* empty *)
-]
 
 let_type_cstr: [
 | DELETE OPT [ ":" lconstr ]
@@ -210,8 +205,6 @@ 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 "]"
@@ -237,8 +230,6 @@ 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: [
@@ -285,13 +276,6 @@ binders_fixannot: [
 | LIST0 binder OPT fixannot
 ]
 
-
-of_type_with_opt_coercion: [
-| DELETE ":>" ">"
-| DELETE ":" ">" ">"
-| DELETE ":" ">"
-]
-
 binder: [
 | DELETE name
 ]
@@ -306,11 +290,15 @@ open_binders: [
 | DELETE closed_binder binders
 ]
 
+type: [
+| operconstr200
+]
+
 closed_binder: [
 | name
 
 | REPLACE "(" name LIST1 name ":" lconstr ")"
-| WITH "(" LIST1 name ":" lconstr ")"
+| WITH "(" LIST1 name ":" type ")"
 | DELETE "(" name ":" lconstr ")"
 
 | DELETE "(" name ":=" lconstr ")"
@@ -324,6 +312,16 @@ closed_binder: [
 | REPLACE "{" name LIST1 name ":" lconstr "}"
 | WITH "{" LIST1 name type_cstr "}"
 | DELETE "{" name ":" lconstr  "}"
+
+| DELETE "[" name "]"
+| DELETE "[" name LIST1 name "]"
+
+| REPLACE "[" name LIST1 name ":" lconstr "]"
+| WITH "[" LIST1 name type_cstr "]"
+| DELETE "[" name ":" lconstr  "]"
+
+| REPLACE "(" Prim.name ":" lconstr "|" lconstr ")"
+| WITH "(" Prim.name ":" type "|" lconstr ")"
 ]
 
 name_colon: [
@@ -377,28 +375,151 @@ eqn: [
 ]
 
 universe_increment: [
-| REPLACE "+" natural
-| WITH OPT ( "+" natural )
-| DELETE (* empty *)
+| OPTINREF
 ]
 
 evar_instance: [
-| REPLACE "@{" LIST1 inst SEP ";" "}"
-| WITH OPT ( "@{" LIST1 inst SEP ";" "}" )
+| OPTINREF
+]
+
+gallina: [
+| REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
+| WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ]
+| DELETE assumptions_token inline assum_list
+| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
+| WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
+|   "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
+|   "Variant" inductive_definition LIST0 ( "with" inductive_definition )
+|   [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition )
+|   "Class" inductive_definition LIST0 ( "with" inductive_definition )
+| REPLACE "Fixpoint" LIST1 rec_definition SEP "with"
+| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
+| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with"
+| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
+| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with"
+| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
+| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with"
+| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
+| REPLACE "Scheme" LIST1 scheme SEP "with"
+| WITH "Scheme" scheme LIST0 ( "with" scheme )
+]
+
+DELETE: [
+| private_token
+| cumulativity_token
+]
+
+opt_coercion: [
+| OPTINREF
+]
+
+opt_constructors_or_fields: [
+| OPTINREF
+]
+
+SPLICE: [
+| opt_coercion
+| opt_constructors_or_fields
+]
+
+constructor_list_or_record_decl: [
+| OPTINREF
+]
+
+record_fields: [
+| REPLACE record_field ";" record_fields
+| WITH LIST1 record_field SEP ";"
+| DELETE record_field
 | DELETE (* empty *)
 ]
 
+decl_notation: [
+| REPLACE "where" LIST1 one_decl_notation SEP decl_sep
+| WITH "where" one_decl_notation LIST0 ( decl_sep one_decl_notation )
+]
+
+assumptions_token: [
+| DELETENT
+]
+
+inline: [
+| REPLACE "Inline" "(" natural ")"
+| WITH "Inline" OPT ( "(" natural ")" )
+| DELETE "Inline"
+| OPTINREF
+]
+
 univ_instance: [
-| DELETE (* empty *)
+| OPTINREF
+]
+
+univ_decl: [
+| REPLACE "@{" LIST0 identref [ "+" | ]     [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+| WITH    "@{" LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
+of_type_with_opt_coercion: [
+| DELETENT
+]
+
+of_type_with_opt_coercion: [
+| [ ":" | ":>" | ":>>" ] type
+]
+
+attribute_value: [
+| OPTINREF
+]
+
+def_body: [
+| DELETE binders ":=" reduce lconstr
+| REPLACE binders ":" lconstr ":=" reduce lconstr
+| WITH LIST0 binder OPT (":" type) ":=" reduce lconstr
+| REPLACE binders ":" lconstr
+| WITH LIST0 binder ":" type
+]
+
+reduce: [
+| OPTINREF
+]
+
+occs: [
+| OPTINREF
+]
+
+delta_flag: [
+| REPLACE "-" "[" LIST1 smart_global "]"
+| WITH OPT "-" "[" LIST1 smart_global "]"
+| DELETE "[" LIST1 smart_global "]"
+| OPTINREF
+]
+
+strategy_flag: [
+| REPLACE OPT delta_flag
+| WITH delta_flag
+| (* empty *)
+| OPTINREF
 ]
 
-constr: [
-| REPLACE "@" global univ_instance
-| WITH "@" global OPT univ_instance
+export_token: [
+| OPTINREF
 ]
 
-(* todo: binders should be binders_opt *)
+functor_app_annot: [
+| OPTINREF
+]
+
+is_module_expr: [
+| OPTINREF
+]
 
+is_module_type: [
+| OPTINREF
+]
+
+gallina_ext: [
+| REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| WITH "Arguments" smart_global LIST0 argument_spec_block    LIST0 [  "," LIST0 more_implicits_block ]                OPT [ ":" LIST1 arguments_modifier SEP "," ]
+]
 
 (* lexer stuff *)
 IDENT: [
@@ -478,6 +599,8 @@ tactic_expr1: [
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO ltac_match_goal match_key OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO ltac_match_term match_key tactic_expr5 "with" match_list "end"
+| REPLACE failkw [ int_or_var | ] LIST0 message_token
+| WITH failkw OPT int_or_var LIST0 message_token
 ]
 
 DELETE: [
@@ -544,12 +667,146 @@ bar_cbrace: [
 | WITH "|}"
 ]
 
+printable: [
+| REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
+| WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string
+| INSERTALL "Print"
+]
+
+command: [
+| REPLACE "Print" printable
+| WITH printable
+| "SubClass" ident_decl def_body
+| REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with"
+| WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body )
+| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with"      (* funind plugin *)
+| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc )      (* funind plugin *)
+| REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
+| WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )      (* funind plugin *)
+
+]
+
+only_parsing: [
+| OPTINREF
+]
+
+syntax: [
+| REPLACE "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
+| WITH    "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ]
+| REPLACE "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
+| WITH    "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ]
+| REPLACE "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
+| WITH    "Reserved" "Infix" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| REPLACE "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
+| WITH    "Reserved" "Notation" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+]
+
+numnotoption: [
+| OPTINREF
+]
+
+binder_tactic: [
+| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
+| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5
+]
+
+tactic_then_gen: [
+| OPTINREF
+]
+
+record_binder_body: [
+| REPLACE binders of_type_with_opt_coercion lconstr
+| WITH binders of_type_with_opt_coercion
+| REPLACE binders of_type_with_opt_coercion lconstr ":=" lconstr
+| WITH binders of_type_with_opt_coercion ":=" lconstr
+]
+
+simple_assum_coe: [
+| REPLACE LIST1 ident_decl of_type_with_opt_coercion lconstr
+| WITH LIST1 ident_decl of_type_with_opt_coercion
+]
+
+constructor_type: [
+| REPLACE binders [ of_type_with_opt_coercion lconstr | ]
+| WITH binders OPT of_type_with_opt_coercion
+]
+
 (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
 (* consider tactic_command vs tac2mode *)
 vernac_aux: [
 | tactic_mode "."
 ]
 
+def_token: [
+| DELETE "SubClass" (* document separately from Definition and Example *)
+]
+
+assumption_token: [
+| REPLACE "Axiom"
+| WITH [ "Axiom" | "Axioms" ]
+| REPLACE "Conjecture"
+| WITH [ "Conjecture" | "Conjectures" ]
+| REPLACE "Hypothesis"
+| WITH [ "Hypothesis" | "Hypotheses" ]
+| REPLACE "Parameter"
+| WITH [ "Parameter" | "Parameters" ]
+| REPLACE "Variable"
+| WITH [ "Variable" | "Variables" ]
+]
+
+legacy_attrs: [
+| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private"
+]
+
+all_attrs: [
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs
+]
+
+vernacular: [
+| LIST0 ( OPT all_attrs [ command | tactic ] "." )
+]
+
+rec_definition: [
+| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
+]
+
+corec_definition: [
+| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
+]
+
+type_cstr: [
+| REPLACE ":" lconstr
+| WITH ":" type
+| OPTINREF
+]
+
+decl_notation: [
+| OPTINREF
+]
+
+inductive_definition: [
+| REPLACE OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation
+| WITH OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation
+]
+
+constructor_list_or_record_decl: [
+| DELETE "|" LIST1 constructor SEP "|"
+| REPLACE identref constructor_type "|" LIST1 constructor SEP "|"
+| WITH OPT "|" LIST1 constructor SEP "|"
+| DELETE identref constructor_type
+| REPLACE identref "{" record_fields "}"
+| WITH OPT identref "{" record_fields "}"
+| DELETE "{" record_fields "}"
+]
+
+record_binder: [
+| REPLACE name record_binder_body
+| WITH name OPT record_binder_body
+| DELETE name
+]
+
 SPLICE: [
 | noedit_mode
 | command_entry
@@ -642,8 +899,6 @@ SPLICE: [
 | tactic
 | uconstr
 | impl_ident_head
-| argument_spec
-| at_level
 | branches
 | check_module_type
 | decorated_vernac
@@ -666,7 +921,27 @@ SPLICE: [
 | evar_instance
 | fix_decls
 | cofix_decls
-]
+| assum_list
+| assum_coe
+| inline
+| occs
+| univ_name_list
+| ltac_info
+| field_mods
+| ltac_production_sep
+| ltac_tactic_level
+| printunivs_subgraph
+| ring_mods
+| scope_delimiter
+| eliminator  (* todo: splice or not? *)
+| quoted_attributes  (* todo: splice or not? *)
+| printable
+| only_parsing
+| def_token
+| record_fields
+| constructor_type
+| record_binder
+] (* end SPLICE *)
 
 RENAME: [
 | clause clause_dft_concl
@@ -711,6 +986,14 @@ RENAME: [
 | corec_definition cofix_definition
 | inst evar_binding
 | univ_instance univ_annot
+| simple_assum_coe assumpt
+| of_type_with_opt_coercion of_type
+| decl_notation decl_notations
+| one_decl_notation decl_notation
+| attribute attr
+| attribute_value attr_value
+| constructor_list_or_record_decl constructors_or_record
+| record_binder_body field_body
 ]
 
 
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 7d18630a02..5fcb56f5f2 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1700,9 +1700,9 @@ let process_rst g file args seen tac_prods cmd_prods =
       let start_index = index_of start !g.order in
       let end_index = index_of end_ !g.order in
       if start_index = None then
-        error "%s line %d: '%s' is undefined\n" file !linenum start;
+        error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum start;
       if end_index = None then
-        error "%s line %d: '%s' is undefined\n" file !linenum end_;
+        error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum end_;
       if start_index <> None && end_index <> None then
         check_range_consistency g start end_;
       match start_index, end_index with
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index e12589bb89..529d81e424 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -322,8 +322,13 @@ closed_binder: [
 | "{" name LIST1 name ":" lconstr "}"
 | "{" name ":" lconstr "}"
 | "{" name LIST1 name "}"
+| "[" name "]"
+| "[" name LIST1 name ":" lconstr "]"
+| "[" name ":" lconstr "]"
+| "[" name LIST1 name "]"
 | "`(" LIST1 typeclass_constraint SEP "," ")"
 | "`{" LIST1 typeclass_constraint SEP "," "}"
+| "`[" LIST1 typeclass_constraint SEP "," "]"
 | "'" pattern0
 ]
 
@@ -643,6 +648,7 @@ command: [
 | "Show" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
+| "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "InjTyp" constr      (* micromega plugin *)
 | "Add" "BinOp" constr      (* micromega plugin *)
 | "Add" "UnOp" constr      (* micromega plugin *)
@@ -937,12 +943,12 @@ opt_constructors_or_fields: [
 ]
 
 inductive_definition: [
-| opt_coercion ident_decl binders OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation
+| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation
 ]
 
 constructor_list_or_record_decl: [
 | "|" LIST1 constructor SEP "|"
-| identref constructor_type "|" LIST0 constructor SEP "|"
+| identref constructor_type "|" LIST1 constructor SEP "|"
 | identref constructor_type
 | identref "{" record_fields "}"
 | "{" record_fields "}"
@@ -1270,7 +1276,7 @@ printable: [
 | "Instances" smart_global
 | "Coercions"
 | "Coercion" "Paths" class_rawexpr class_rawexpr
-| "Canonical" "Projections"
+| "Canonical" "Projections" LIST0 smart_global
 | "Typing" "Flags"
 | "Tables"
 | "Options"
@@ -1400,8 +1406,7 @@ syntax_modifier: [
 | "only" "parsing"
 | "format" STRING OPT STRING
 | IDENT; "," LIST1 IDENT SEP "," "at" level
-| IDENT; "at" level
-| IDENT; "at" level constr_as_binder_kind
+| IDENT; "at" level OPT constr_as_binder_kind
 | IDENT constr_as_binder_kind
 | IDENT syntax_extension_type
 ]
@@ -1412,17 +1417,18 @@ syntax_extension_type: [
 | "bigint"
 | "binder"
 | "constr"
-| "constr" OPT at_level OPT constr_as_binder_kind
+| "constr" at_level_opt OPT constr_as_binder_kind
 | "pattern"
 | "pattern" "at" "level" natural
 | "strict" "pattern"
 | "strict" "pattern" "at" "level" natural
 | "closed" "binder"
-| "custom" IDENT OPT at_level OPT constr_as_binder_kind
+| "custom" IDENT at_level_opt OPT constr_as_binder_kind
 ]
 
-at_level: [
+at_level_opt: [
 | "at" level
+|
 ]
 
 constr_as_binder_kind: [
@@ -1719,7 +1725,6 @@ simple_tactic: [
 | "restart_timer" OPT string
 | "finish_timing" OPT string
 | "finish_timing" "(" string ")" OPT string
-| "myred"      (* micromega plugin *)
 | "psatz_Z" int_or_var tactic      (* micromega plugin *)
 | "psatz_Z" tactic      (* micromega plugin *)
 | "xlia" tactic      (* micromega plugin *)
@@ -1735,13 +1740,12 @@ simple_tactic: [
 | "psatz_R" tactic      (* micromega plugin *)
 | "psatz_Q" int_or_var tactic      (* micromega plugin *)
 | "psatz_Q" tactic      (* micromega plugin *)
-| "iter_specs" tactic      (* micromega plugin *)
+| "zify_iter_specs" tactic      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
-| "saturate"      (* micromega plugin *)
+| "zify_saturate"      (* micromega plugin *)
+| "zify_iter_let" tactic      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
-| "omega" "with" LIST1 ident      (* omega plugin *)
-| "omega" "with" "*"      (* omega plugin *)
 | "rtauto"
 | "protect_fv" string "in" ident      (* setoid_ring plugin *)
 | "protect_fv" string      (* setoid_ring plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 63e0ca129c..908e3ccd51 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -29,7 +29,7 @@ vernac_control: [
 | "Redirect" string vernac_control
 | "Timeout" num vernac_control
 | "Fail" vernac_control
-| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) vernac
+| LIST0 ( "#[" LIST0 attr SEP "," "]" ) vernac
 ]
 
 term: [
@@ -102,50 +102,24 @@ dangling_pattern_extension_rule: [
 | "@" "?" ident LIST1 ident
 ]
 
-record_fields: [
-| record_field ";" record_fields
-| record_field
-|
-]
-
-record_field: [
-| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) record_binder OPT [ "|" num ] decl_notation
-]
-
-decl_notation: [
-| "where" LIST1 one_decl_notation SEP "and"
-|
-]
-
-one_decl_notation: [
-| string ":=" term1_extended OPT [ ":" ident ]
+assumption_token: [
+| [ "Axiom" | "Axioms" ]
+| [ "Conjecture" | "Conjectures" ]
+| [ "Parameter" | "Parameters" ]
+| [ "Hypothesis" | "Hypotheses" ]
+| [ "Variable" | "Variables" ]
 ]
 
-record_binder: [
-| name
-| name record_binder_body
+assumpt: [
+| LIST1 ident_decl of_type
 ]
 
-record_binder_body: [
-| 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: [
-| ":>>"
-| ":>"
-| ":"
+ident_decl: [
+| ident OPT univ_decl
 ]
 
-attribute: [
-| ident attribute_value
-]
-
-attribute_value: [
-| "=" string
-| "(" LIST0 attribute SEP "," ")"
-|
+of_type: [
+| [ ":" | ":>" | ":>>" ] type
 ]
 
 qualid: [
@@ -156,6 +130,10 @@ field_ident: [
 | "." ident
 ]
 
+type: [
+| term
+]
+
 numeral: [
 | LIST1 digit OPT ( "." LIST1 digit ) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
 ]
@@ -184,6 +162,27 @@ subsequent_letter: [
 | [ first_letter | digit | "'" | unicode_id_part ]
 ]
 
+vernacular: [
+| LIST0 ( OPT all_attrs [ command | ltac_expr ] "." )
+]
+
+all_attrs: [
+| LIST0 ( "#[" LIST0 attr SEP "," "]" ) OPT legacy_attrs
+]
+
+attr: [
+| ident OPT attr_value
+]
+
+attr_value: [
+| "=" string
+| "(" LIST0 attr SEP "," ")"
+]
+
+legacy_attrs: [
+| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private"
+]
+
 sort: [
 | "Set"
 | "Prop"
@@ -208,6 +207,10 @@ universe_name: [
 | "Prop"
 ]
 
+univ_annot: [
+| "@{" LIST0 universe_level "}"
+]
+
 universe_level: [
 | "Set"
 | "Prop"
@@ -216,8 +219,12 @@ universe_level: [
 | qualid
 ]
 
-univ_annot: [
-| "@{" LIST0 universe_level "}"
+univ_decl: [
+| "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
+univ_constraint: [
+| universe_name [ "<" | "=" | "<=" ] universe_name
 ]
 
 term_fix: [
@@ -226,7 +233,7 @@ term_fix: [
 ]
 
 fix_body: [
-| ident LIST0 binder OPT fixannot OPT ( ":" term ) ":=" term
+| ident LIST0 binder OPT fixannot OPT ( ":" type ) ":=" term
 ]
 
 fixannot: [
@@ -246,12 +253,12 @@ term_cofix: [
 ]
 
 cofix_body: [
-| ident LIST0 binder OPT ( ":" term ) ":=" term
+| ident LIST0 binder OPT ( ":" type ) ":=" term
 ]
 
 term_let: [
-| "let" name OPT ( ":" term ) ":=" term "in" term
-| "let" name LIST1 binder OPT ( ":" term ) ":=" term "in" term
+| "let" name OPT ( ":" type ) ":=" term "in" term
+| "let" name LIST1 binder OPT ( ":" type ) ":=" 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
@@ -269,13 +276,15 @@ name: [
 
 binder: [
 | name
-| "(" LIST1 name ":" term ")"
-| "(" name OPT ( ":" term ) ":=" term ")"
-| "{" LIST1 name OPT ( ":" term ) "}"
+| "(" LIST1 name ":" type ")"
+| "(" name OPT ( ":" type ) ":=" term ")"
+| "(" name ":" type "|" term ")"
+| "{" LIST1 name OPT ( ":" type ) "}"
+| "[" LIST1 name OPT ( ":" type ) "]"
 | "`(" LIST1 typeclass_constraint SEP "," ")"
 | "`{" LIST1 typeclass_constraint SEP "," "}"
+| "`[" LIST1 typeclass_constraint SEP "," "]"
 | "'" pattern0
-| "(" name ":" term "|" term ")"
 ]
 
 typeclass_constraint: [
@@ -359,17 +368,20 @@ subprf: [
 ]
 
 gallina: [
-| 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
+| thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
+| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
+| [ "Definition" | "Example" ] ident_decl def_body
 | "Let" ident def_body
-| 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"
+| "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
+| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
+| "Variant" inductive_definition LIST0 ( "with" inductive_definition )
+| [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition )
+| "Class" inductive_definition LIST0 ( "with" inductive_definition )
+| "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
+| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
+| "Scheme" scheme LIST0 ( "with" scheme )
 | "Combined" "Scheme" ident "from" LIST1 ident SEP ","
 | "Register" qualid "as" qualid
 | "Register" "Inline" qualid
@@ -380,7 +392,15 @@ gallina: [
 ]
 
 fix_definition: [
-| ident_decl LIST0 binder OPT fixannot OPT ( ":" term ) OPT [ ":=" term ] decl_notation
+| ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
+]
+
+decl_notations: [
+| "where" decl_notation LIST0 ( "and" decl_notation )
+]
+
+decl_notation: [
+| string ":=" term1_extended OPT [ ":" ident ]
 ]
 
 register_token: [
@@ -444,80 +464,23 @@ thm_token: [
 | "Property"
 ]
 
-def_token: [
-| "Definition"
-| "Example"
-| "SubClass"
-]
-
-assumption_token: [
-| "Hypothesis"
-| "Variable"
-| "Axiom"
-| "Parameter"
-| "Conjecture"
-]
-
-assumptions_token: [
-| "Hypotheses"
-| "Variables"
-| "Axioms"
-| "Parameters"
-| "Conjectures"
-]
-
-inline: [
-| "Inline" "(" num ")"
-| "Inline"
-|
-]
-
-univ_constraint: [
-| universe_name [ "<" | "=" | "<=" ] universe_name
-]
-
-ident_decl: [
-| ident OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] )
-]
-
-finite_token: [
-| "Inductive"
-| "CoInductive"
-| "Variant"
-| "Record"
-| "Structure"
-| "Class"
-]
-
-cumulativity_token: [
-| "Cumulative"
-| "NonCumulative"
-]
-
-private_token: [
-| "Private"
-|
-]
-
 def_body: [
-| LIST0 binder ":=" reduce term
-| LIST0 binder ":" term ":=" reduce term
-| LIST0 binder ":" term
+| LIST0 binder OPT ( ":" type ) ":=" OPT reduce term
+| LIST0 binder ":" type
 ]
 
 reduce: [
 | "Eval" red_expr "in"
-|
 ]
 
 red_expr: [
 | "red"
 | "hnf"
-| "simpl" delta_flag OPT ref_or_pattern_occ
-| "cbv" strategy_flag
-| "cbn" strategy_flag
-| "lazy" strategy_flag
-| "compute" delta_flag
+| "simpl" OPT delta_flag OPT ref_or_pattern_occ
+| "cbv" OPT strategy_flag
+| "cbn" OPT strategy_flag
+| "lazy" OPT strategy_flag
+| "compute" OPT delta_flag
 | "vm_compute" OPT ref_or_pattern_occ
 | "native_compute" OPT ref_or_pattern_occ
 | "unfold" LIST1 unfold_occ SEP ","
@@ -526,6 +489,19 @@ red_expr: [
 | ident
 ]
 
+delta_flag: [
+| OPT "-" "[" LIST1 smart_global "]"
+]
+
+smart_global: [
+| qualid
+| by_notation
+]
+
+by_notation: [
+| string OPT [ "%" ident ]
+]
+
 strategy_flag: [
 | LIST1 red_flags
 | delta_flag
@@ -538,70 +514,71 @@ red_flags: [
 | "fix"
 | "cofix"
 | "zeta"
-| "delta" delta_flag
+| "delta" OPT delta_flag
 ]
 
-delta_flag: [
-| "-" "[" LIST1 smart_global "]"
-| "[" LIST1 smart_global "]"
-|
+ref_or_pattern_occ: [
+| smart_global OPT ( "at" occs_nums )
+| term1_extended OPT ( "at" occs_nums )
 ]
 
-ref_or_pattern_occ: [
-| smart_global occs
-| term1_extended occs
+occs_nums: [
+| LIST1 num_or_var
+| "-" num_or_var LIST0 int_or_var
 ]
 
-unfold_occ: [
-| smart_global occs
+num_or_var: [
+| num
+| ident
 ]
 
-opt_constructors_or_fields: [
-| ":=" constructor_list_or_record_decl
-|
+int_or_var: [
+| int
+| ident
 ]
 
-inductive_definition: [
-| opt_coercion ident_decl LIST0 binder OPT [ ":" term ] opt_constructors_or_fields decl_notation
+unfold_occ: [
+| smart_global OPT ( "at" occs_nums )
 ]
 
-opt_coercion: [
-| ">"
-|
+pattern_occ: [
+| term1_extended OPT ( "at" occs_nums )
 ]
 
-constructor_list_or_record_decl: [
-| "|" LIST1 constructor SEP "|"
-| ident constructor_type "|" LIST0 constructor SEP "|"
-| ident constructor_type
-| ident "{" record_fields "}"
-| "{" record_fields "}"
-|
+finite_token: [
+| "Inductive"
+| "CoInductive"
+| "Variant"
+| "Record"
+| "Structure"
+| "Class"
 ]
 
-assum_list: [
-| LIST1 assum_coe
-| simple_assum_coe
+inductive_definition: [
+| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]
 
-assum_coe: [
-| "(" simple_assum_coe ")"
+constructors_or_record: [
+| OPT "|" LIST1 constructor SEP "|"
+| OPT ident "{" LIST1 record_field SEP ";" "}"
 ]
 
-simple_assum_coe: [
-| LIST1 ident_decl of_type_with_opt_coercion term
+constructor: [
+| ident LIST0 binder OPT of_type
 ]
 
-constructor_type: [
-| LIST0 binder [ of_type_with_opt_coercion term | ]
+record_field: [
+| LIST0 ( "#[" LIST0 attr SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
 ]
 
-constructor: [
-| ident constructor_type
+field_body: [
+| LIST0 binder of_type
+| LIST0 binder of_type ":=" term
+| LIST0 binder ":=" term
 ]
 
 cofix_definition: [
-| ident_decl LIST0 binder OPT ( ":" term ) OPT [ ":=" term ] decl_notation
+| ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
 
 scheme: [
@@ -624,25 +601,16 @@ sort_family: [
 | "Type"
 ]
 
-smart_global: [
-| qualid
-| by_notation
-]
-
-by_notation: [
-| string OPT [ "%" ident ]
-]
-
 gallina_ext: [
-| "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
+| "Module" OPT export_token ident LIST0 module_binder of_module_type OPT is_module_expr
+| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT is_module_type
+| "Declare" "Module" OPT export_token ident LIST0 module_binder ":" module_type_inl
 | "Section" ident
 | "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
-| "Require" export_token LIST1 qualid
-| "From" qualid "Require" export_token LIST1 qualid
+| "Require" OPT export_token LIST1 qualid
+| "From" qualid "Require" OPT export_token LIST1 qualid
 | "Import" LIST1 qualid
 | "Export" LIST1 qualid
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
@@ -650,9 +618,9 @@ gallina_ext: [
 | "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" qualid OPT [ OPT univ_decl def_body ]
 | "Canonical" OPT "Structure" by_notation
-| "Coercion" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body
+| "Coercion" qualid OPT univ_decl def_body
 | "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr
 | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
@@ -661,7 +629,7 @@ gallina_ext: [
 | "Existing" "Instance" qualid hint_info
 | "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
 | "Existing" "Class" qualid
-| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
+| "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
 | "Implicit" "Type" reserv_list
 | "Implicit" "Types" reserv_list
 | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ]
@@ -689,43 +657,41 @@ hint_info: [
 export_token: [
 | "Import"
 | "Export"
-|
 ]
 
-of_module_type: [
-| ":" module_type_inl
-| LIST0 ( "<:" module_type_inl )
+module_binder: [
+| "(" OPT export_token LIST1 ident ":" module_type_inl ")"
 ]
 
-is_module_type: [
-| ":=" module_type_inl LIST0 ( "<+" module_type_inl )
-|
+module_type_inl: [
+| "!" module_type
+| module_type OPT functor_app_annot
 ]
 
-is_module_expr: [
-| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl )
-|
+module_type: [
+| qualid
+| "(" module_type ")"
+| module_type module_expr_atom
+| module_type "with" with_declaration
+]
+
+with_declaration: [
+| "Definition" qualid OPT univ_decl ":=" term
+| "Module" qualid ":=" qualid
 ]
 
 functor_app_annot: [
 | "[" "inline" "at" "level" num "]"
 | "[" "no" "inline" "]"
-|
-]
-
-module_expr_inl: [
-| "!" module_expr
-| module_expr functor_app_annot
 ]
 
-module_type_inl: [
-| "!" module_type
-| module_type functor_app_annot
+of_module_type: [
+| ":" module_type_inl
+| LIST0 ( "<:" module_type_inl )
 ]
 
-module_expr: [
-| module_expr_atom
-| module_expr module_expr_atom
+is_module_type: [
+| ":=" module_type_inl LIST0 ( "<+" module_type_inl )
 ]
 
 module_expr_atom: [
@@ -733,25 +699,31 @@ module_expr_atom: [
 | "(" module_expr ")"
 ]
 
-module_type: [
-| qualid
-| "(" module_type ")"
-| module_type module_expr_atom
-| module_type "with" with_declaration
+module_expr: [
+| module_expr_atom
+| module_expr module_expr_atom
 ]
 
-with_declaration: [
-| "Definition" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) ":=" term
-| "Module" qualid ":=" qualid
+is_module_expr: [
+| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl )
+]
+
+module_expr_inl: [
+| "!" module_expr
+| module_expr OPT functor_app_annot
 ]
 
 argument_spec_block: [
-| OPT "!" name OPT ( "%" ident )
+| argument_spec
 | "/"
 | "&"
-| "(" LIST1 ( OPT "!" name OPT ( "%" ident ) ) ")" OPT ( "%" ident )
-| "[" LIST1 ( OPT "!" name OPT ( "%" ident ) ) "]" OPT ( "%" ident )
-| "{" LIST1 ( OPT "!" name OPT ( "%" ident ) ) "}" OPT ( "%" ident )
+| "(" LIST1 argument_spec ")" OPT ( "%" ident )
+| "[" LIST1 argument_spec "]" OPT ( "%" ident )
+| "{" LIST1 argument_spec "}" OPT ( "%" ident )
+]
+
+argument_spec: [
+| OPT "!" name OPT ( "%" ident )
 ]
 
 more_implicits_block: [
@@ -760,6 +732,20 @@ more_implicits_block: [
 | "{" LIST1 name "}"
 ]
 
+arguments_modifier: [
+| "simpl" "nomatch"
+| "simpl" "never"
+| "default" "implicits"
+| "clear" "bidirectionality" "hint"
+| "clear" "implicits"
+| "clear" "scopes"
+| "clear" "scopes" "and" "implicits"
+| "clear" "implicits" "and" "scopes"
+| "rename"
+| "assert"
+| "extra" "scopes"
+]
+
 strategy_level: [
 | "expand"
 | "opaque"
@@ -785,20 +771,6 @@ simple_reserv: [
 | LIST1 ident ":" term
 ]
 
-arguments_modifier: [
-| "simpl" "nomatch"
-| "simpl" "never"
-| "default" "implicits"
-| "clear" "implicits"
-| "clear" "scopes"
-| "clear" "bidirectionality" "hint"
-| "rename"
-| "assert"
-| "extra" "scopes"
-| "clear" "scopes" "and" "implicits"
-| "clear" "implicits" "and" "scopes"
-]
-
 command: [
 | "Goal" term
 | "Declare" "Scope" ident
@@ -812,7 +784,43 @@ command: [
 | "Add" "Rec" "LoadPath" string as_dirpath
 | "Remove" "LoadPath" string
 | "Type" term
-| "Print" printable
+| "Print" "Term" smart_global OPT ( "@{" LIST0 name "}" )
+| "Print" "All"
+| "Print" "Section" qualid
+| "Print" "Grammar" ident
+| "Print" "Custom" "Grammar" ident
+| "Print" "LoadPath" OPT dirpath
+| "Print" "Modules"
+| "Print" "Libraries"
+| "Print" "ML" "Path"
+| "Print" "ML" "Modules"
+| "Print" "Debug" "GC"
+| "Print" "Graph"
+| "Print" "Classes"
+| "Print" "TypeClasses"
+| "Print" "Instances" smart_global
+| "Print" "Coercions"
+| "Print" "Coercion" "Paths" class_rawexpr class_rawexpr
+| "Print" "Canonical" "Projections" LIST0 smart_global
+| "Print" "Typing" "Flags"
+| "Print" "Tables"
+| "Print" "Options"
+| "Print" "Hint"
+| "Print" "Hint" smart_global
+| "Print" "Hint" "*"
+| "Print" "HintDb" ident
+| "Print" "Scopes"
+| "Print" "Scope" ident
+| "Print" "Visibility" OPT ident
+| "Print" "Implicit" smart_global
+| "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
+| "Print" "Assumptions" smart_global
+| "Print" "Opaque" "Dependencies" smart_global
+| "Print" "Transparent" "Dependencies" smart_global
+| "Print" "All" "Dependencies" smart_global
+| "Print" "Strategy" smart_global
+| "Print" "Strategies"
+| "Print" "Registered"
 | "Print" smart_global OPT ( "@{" LIST0 name "}" )
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
@@ -931,6 +939,7 @@ command: [
 | "Show" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" "CutOff" int
 | "Show" "Ltac" "Profile" string
+| "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "InjTyp" term1_extended      (* micromega plugin *)
 | "Add" "BinOp" term1_extended      (* micromega plugin *)
 | "Add" "UnOp" term1_extended      (* micromega plugin *)
@@ -959,12 +968,12 @@ command: [
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
 | "Locate" "Ltac" qualid
-| "Ltac" LIST1 tacdef_body SEP "with"
+| "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
 | "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 *)
+| "Function" fix_definition LIST0 ( "with" fix_definition )
+| "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )
 | "Extraction" qualid      (* extraction plugin *)
 | "Recursive" "Extraction" LIST1 qualid      (* extraction plugin *)
 | "Extraction" string LIST1 qualid      (* extraction plugin *)
@@ -1002,8 +1011,9 @@ command: [
 | "Print" "Rings"      (* 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
+| "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption
 | "String" "Notation" qualid qualid qualid ":" ident
+| "SubClass" ident_decl def_body
 ]
 
 orient: [
@@ -1043,46 +1053,6 @@ starredidentref: [
 | "Type" "*"
 ]
 
-printable: [
-| "Term" smart_global OPT ( "@{" LIST0 name "}" )
-| "All"
-| "Section" qualid
-| "Grammar" ident
-| "Custom" "Grammar" ident
-| "LoadPath" OPT dirpath
-| "Modules"
-| "Libraries"
-| "ML" "Path"
-| "ML" "Modules"
-| "Debug" "GC"
-| "Graph"
-| "Classes"
-| "TypeClasses"
-| "Instances" smart_global
-| "Coercions"
-| "Coercion" "Paths" class_rawexpr class_rawexpr
-| "Canonical" "Projections"
-| "Typing" "Flags"
-| "Tables"
-| "Options"
-| "Hint"
-| "Hint" smart_global
-| "Hint" "*"
-| "HintDb" ident
-| "Scopes"
-| "Scope" ident
-| "Visibility" OPT ident
-| "Implicit" smart_global
-| [ "Sorted" | ] "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
-| "Assumptions" smart_global
-| "Opaque" "Dependencies" smart_global
-| "Transparent" "Dependencies" smart_global
-| "All" "Dependencies" smart_global
-| "Strategy" smart_global
-| "Strategies"
-| "Registered"
-]
-
 dirpath: [
 | ident
 | dirpath field_ident
@@ -1160,7 +1130,6 @@ ltac_production_item: [
 ]
 
 numnotoption: [
-|
 | "(" "warning" "after" num ")"
 | "(" "abstract" "after" num ")"
 ]
@@ -1288,17 +1257,12 @@ syntax: [
 | "Delimit" "Scope" ident "with" ident
 | "Undelimit" "Scope" ident
 | "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 ]
+| "Infix" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
+| "Notation" ident LIST0 ident ":=" term1_extended OPT ( "(" "only" "parsing" ")" )
+| "Notation" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
 | "Format" "Notation" string string string
-| "Reserved" "Infix" string [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-| "Reserved" "Notation" string [ "(" LIST1 syntax_modifier SEP "," ")" | ]
-]
-
-only_parsing: [
-| "(" "only" "parsing" ")"
-|
+| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
+| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
 ]
 
 level: [
@@ -1317,31 +1281,35 @@ syntax_modifier: [
 | "only" "parsing"
 | "format" string OPT string
 | ident "," LIST1 ident SEP "," "at" level
-| ident "at" level
-| ident "at" level constr_as_binder_kind
+| ident "at" level OPT constr_as_binder_kind
 | ident constr_as_binder_kind
 | ident syntax_extension_type
 ]
 
+constr_as_binder_kind: [
+| "as" "ident"
+| "as" "pattern"
+| "as" "strict" "pattern"
+]
+
 syntax_extension_type: [
 | "ident"
 | "global"
 | "bigint"
 | "binder"
 | "constr"
-| "constr" OPT ( "at" level ) OPT constr_as_binder_kind
+| "constr" at_level_opt OPT constr_as_binder_kind
 | "pattern"
 | "pattern" "at" "level" num
 | "strict" "pattern"
 | "strict" "pattern" "at" "level" num
 | "closed" "binder"
-| "custom" ident OPT ( "at" level ) OPT constr_as_binder_kind
+| "custom" ident at_level_opt OPT constr_as_binder_kind
 ]
 
-constr_as_binder_kind: [
-| "as" "ident"
-| "as" "pattern"
-| "as" "strict" "pattern"
+at_level_opt: [
+| "at" level
+|
 ]
 
 simple_tactic: [
@@ -1591,7 +1559,7 @@ simple_tactic: [
 | "eenough" term1_extended as_ipat by_tactic
 | "generalize" term1_extended
 | "generalize" term1_extended LIST1 term1_extended
-| "generalize" term1_extended occs as_name LIST0 [ "," pattern_occ as_name ]
+| "generalize" term1_extended OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ]
 | "induction" induction_clause_list
 | "einduction" induction_clause_list
 | "destruct" induction_clause_list
@@ -1605,11 +1573,11 @@ simple_tactic: [
 | "inversion" quantified_hypothesis "using" term1_extended in_hyp_list
 | "red" clause_dft_concl
 | "hnf" 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
+| "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
+| "cbv" OPT strategy_flag clause_dft_concl
+| "cbn" OPT strategy_flag clause_dft_concl
+| "lazy" OPT strategy_flag clause_dft_concl
+| "compute" OPT delta_flag 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
@@ -1631,7 +1599,6 @@ simple_tactic: [
 | "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 *)
 | "xlia" ltac_expr      (* micromega plugin *)
@@ -1647,24 +1614,18 @@ simple_tactic: [
 | "psatz_R" ltac_expr      (* micromega plugin *)
 | "psatz_Q" int_or_var ltac_expr      (* micromega plugin *)
 | "psatz_Q" ltac_expr      (* micromega plugin *)
-| "iter_specs" ltac_expr      (* micromega plugin *)
+| "zify_iter_specs" ltac_expr      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
-| "saturate"      (* micromega plugin *)
+| "zify_saturate"      (* micromega plugin *)
+| "zify_iter_let" ltac_expr      (* micromega plugin *)
 | "nsatz_compute" term1_extended      (* nsatz plugin *)
 | "omega"      (* 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 "[" 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: [
-| int
-| ident
-]
-
 hloc: [
 |
 | "in" "|-" "*"
@@ -1686,17 +1647,12 @@ by_arg_tac: [
 
 in_clause: [
 | in_clause
-| "*" occs
+| "*" OPT ( "at" occs_nums )
 | "*" "|-" concl_occ
 | LIST0 hypident_occ SEP "," "|-" concl_occ
 | LIST0 hypident_occ SEP ","
 ]
 
-occs: [
-| "at" occs_nums
-|
-]
-
 as_ipat: [
 | "as" simple_intropattern
 |
@@ -1809,10 +1765,6 @@ bindings: [
 | LIST1 term1_extended
 ]
 
-pattern_occ: [
-| term1_extended occs
-]
-
 comparison: [
 | "="
 | "<"
@@ -1838,12 +1790,12 @@ hypident: [
 ]
 
 hypident_occ: [
-| hypident occs
+| hypident OPT ( "at" occs_nums )
 ]
 
 clause_dft_concl: [
 | "in" in_clause
-| occs
+| OPT ( "at" occs_nums )
 |
 ]
 
@@ -1858,18 +1810,8 @@ opt_clause: [
 |
 ]
 
-occs_nums: [
-| LIST1 num_or_var
-| "-" num_or_var LIST0 int_or_var
-]
-
-num_or_var: [
-| num
-| ident
-]
-
 concl_occ: [
-| "*" occs
+| "*" OPT ( "at" occs_nums )
 |
 ]
 
@@ -1987,7 +1929,7 @@ ltac_expr: [
 
 binder_tactic: [
 | "fun" LIST1 fun_var "=>" ltac_expr
-| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr
+| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
 | "info" ltac_expr
 ]
 
@@ -2005,16 +1947,15 @@ let_clause: [
 ltac_expr4: [
 | ltac_expr3 ";" binder_tactic
 | ltac_expr3 ";" ltac_expr3
-| ltac_expr3 ";" "[" multi_goal_tactics "]"
-| ltac_expr3 ";" "[" ">" multi_goal_tactics "]"
+| ltac_expr3 ";" "[" OPT multi_goal_tactics "]"
 | ltac_expr3
+| ltac_expr3 ";" "[" ">" OPT multi_goal_tactics "]"
 ]
 
 multi_goal_tactics: [
 | OPT ltac_expr "|" multi_goal_tactics
 | ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
 | ltac_expr
-|
 ]
 
 ltac_expr_opt: [
@@ -2044,6 +1985,20 @@ ltac_expr3: [
 | ltac_expr2
 ]
 
+only_selector: [
+| "only" selector ":"
+]
+
+selector: [
+| LIST1 range_selector SEP ","
+| "[" ident "]"
+]
+
+range_selector: [
+| num "-" num
+| num
+]
+
 ltac_expr2: [
 | ltac_expr1 "+" binder_tactic
 | ltac_expr1 "+" ltac_expr2
@@ -2058,7 +2013,7 @@ ltac_expr1: [
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
 | "idtac" LIST0 message_token
-| failkw [ int_or_var | ] LIST0 message_token
+| failkw OPT int_or_var LIST0 message_token
 | ltac_match_goal
 | simple_tactic
 | tactic_arg
@@ -2099,7 +2054,7 @@ tactic_arg_compat: [
 
 ltac_expr0: [
 | "(" ltac_expr ")"
-| "[>" multi_goal_tactics "]"
+| "[>" OPT multi_goal_tactics "]"
 | tactic_atom
 ]
 
@@ -2115,20 +2070,6 @@ toplevel_selector: [
 | "!" ":"
 ]
 
-only_selector: [
-| "only" selector ":"
-]
-
-selector: [
-| LIST1 range_selector SEP ","
-| "[" ident "]"
-]
-
-range_selector: [
-| num "-" num
-| num
-]
-
 ltac_match_term: [
 | match_key ltac_expr "with" OPT "|" LIST1 match_rule SEP "|" "end"
 ]
diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg
index 8170b71e7a..93eb38d1a0 100644
--- a/doc/tools/docgram/productionlist.edit_mlg
+++ b/doc/tools/docgram/productionlist.edit_mlg
@@ -12,19 +12,3 @@
 (* Contents used to generate productionlists in doc *)
 
 DOC_GRAMMAR
-
-(* this is here because they're inside _opt generated by EXPAND *)
-SPLICE: [
-| ltac_info
-| eliminator
-| field_mods
-| ltac_production_sep
-| ltac_tactic_level
-| module_binder
-| printunivs_subgraph
-| quoted_attributes
-| ring_mods
-| scope_delimiter
-| univ_decl
-| univ_name_list
-]