diff options
| author | Jim Fehrle | 2019-12-18 23:23:34 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-12-28 12:34:47 -0800 |
| commit | 7b143ed46ab2b1b804b834b59533bef5960be9bc (patch) | |
| tree | 97736e1de02a980f21880f4466009707e71821f8 /doc/tools/docgram/orderedGrammar | |
| parent | bdb5150669d5ac972d3d2b3c9cc2045e77dc9ad5 (diff) | |
Convert productionlists to prodns
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 1714 |
1 files changed, 413 insertions, 1301 deletions
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 ] |