Convert Gallina Vernac to use prodn

1 files changed, 290 insertions, 349 deletions

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