diff options
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 4170 |
1 files changed, 4170 insertions, 0 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar new file mode 100644 index 0000000000..cd6e11505c --- /dev/null +++ b/doc/tools/docgram/orderedGrammar @@ -0,0 +1,4170 @@ +(* Defines the order to apply to editedGrammar to get productionlistGrammar. +doc_grammar will modify this file to add/remove nonterminals and productions +to match editedGrammar, which will remove comments. Not compiled into Coq *) +DOC_GRAMMAR + +global: [ +| reference +] + +constr_pattern: [ +| term +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| empty +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" universe_expr_list_comma ")" +| universe_expr +] + +universe_expr_list_comma: [ +| universe_expr_list_comma "," universe_expr +| universe_expr +] + +lconstr: [ +| operconstr200 +| lconstr +] + +term: [ +| operconstr8 +| "@" global instance +] + +operconstr200: [ +| binder_constr +| operconstr100 +] + +operconstr100: [ +| operconstr99 "<:" binder_constr +| operconstr99 "<:" operconstr100 +| operconstr99 "<<:" binder_constr +| operconstr99 "<<:" operconstr100 +| operconstr99 ":" binder_constr +| operconstr99 ":" operconstr100 +| operconstr99 ":>" +| operconstr99 +] + +operconstr99: [ +| operconstr90 +] + +operconstr90: [ +| operconstr10 +] + +operconstr10: [ +| operconstr9 appl_arg_list +| "@" global instance operconstr9_list_opt +| "@" pattern_identref ident_list +| operconstr9 +] + +appl_arg_list: [ +| appl_arg_list appl_arg +| appl_arg +] + +operconstr9: [ +| ".." operconstr0 ".." +| operconstr8 +] + +operconstr8: [ +| operconstr1 +] + +operconstr1: [ +| operconstr0 ".(" global appl_arg_list_opt ")" +| operconstr0 ".(" "@" global operconstr9_list_opt ")" +| operconstr0 "%" IDENT +| operconstr0 +] + +appl_arg_list_opt: [ +| appl_arg_list_opt appl_arg +| empty +] + +operconstr9_list_opt: [ +| operconstr9_list_opt operconstr9 +| empty +] + +operconstr0: [ +| atomic_constr +| match_constr +| "(" operconstr200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" operconstr200 "}" +| "`(" operconstr200 ")" +| "ltac" ":" "(" ltac_expr ")" +] + +record_declaration: [ +| record_fields +] + +record_fields: [ +| record_field_declaration ";" record_fields +| record_field_declaration +| empty +| record_field ";" record_fields +| record_field ";" +| record_field +] + +record_field_declaration: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," operconstr200 +| "fun" open_binders "=>" operconstr200 +| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200 +| "let" single_fix "in" operconstr200 +| "let" name_alt return_type ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| fix_constr +| "if" operconstr200 "is" ssr_dthen ssr_else (* ssr plugin *) +| "if" operconstr200 "isn't" ssr_dthen ssr_else (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +] + +name_alt: [ +| "(" name_list_comma_opt ")" +| "()" +] + +name_list_comma_opt: [ +| name_list_comma +| empty +] + +name_list_comma: [ +| name_list_comma "," name +| name +] + +name_list_opt: [ +| name_list_opt name +| empty +] + +name_list: [ +| name_list name +| name +] + +appl_arg: [ +| lpar_id_coloneq lconstr ")" +| operconstr9 +] + +atomic_constr: [ +| global instance +| sort +| NUMERAL +| string +| "_" +| "?" "[" ident "]" +| "?" "[" "?" ident "]" +| "?" ident evar_instance +] + +inst: [ +| ident ":=" lconstr +] + +evar_instance: [ +| "@{" inst_list_semi "}" +| empty +] + +inst_list_semi: [ +| inst_list_semi ";" inst +| inst +] + +instance: [ +| "@{" universe_level_list_opt "}" +| empty +] + +universe_level_list_opt: [ +| universe_level_list_opt universe_level +| empty +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_constr: [ +| single_fix +| single_fix "with" fix_decl_list "for" ident +] + +fix_decl_list: [ +| fix_decl_list "with" fix_decl +| fix_decl +] + +single_fix: [ +| fix_kw fix_decl +] + +fix_kw: [ +| "fix" +| "cofix" +] + +fix_decl: [ +| ident binders_fixannot type_cstr ":=" operconstr200 +] + +match_constr: [ +| "match" case_item_list_comma case_type_opt "with" branches "end" +] + +case_item_list_comma: [ +| case_item_list_comma "," case_item +| case_item +] + +case_type_opt: [ +| case_type +| empty +] + +case_item: [ +| operconstr100 as_opt in_opt +] + +as_opt2: [ +| as_opt case_type +| empty +] + +in_opt: [ +| "in" pattern200 +| empty +] + +case_type: [ +| "return" operconstr100 +] + +return_type: [ +| as_opt2 +] + +as_opt3: [ +| "as" dirpath +| empty +] + +branches: [ +| or_opt eqn_list_or_opt +] + +mult_pattern: [ +| pattern200_list_comma +] + +pattern200_list_comma: [ +| pattern200_list_comma "," pattern200 +| pattern200 +] + +eqn: [ +| mult_pattern_list_or "=>" lconstr +] + +mult_pattern_list_or: [ +| mult_pattern_list_or "|" mult_pattern +| mult_pattern +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern ";" +| record_pattern +| empty +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" binder_constr +| pattern99 ":" operconstr100 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 pattern1_list +| "@" reference pattern1_list_opt +| pattern1 +] + +pattern1_list: [ +| pattern1_list pattern1 +| pattern1 +] + +pattern1_list_opt: [ +| pattern1_list_opt pattern1 +| empty +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" pattern200_list_or ")" +| NUMERAL +| string +] + +pattern200_list_or: [ +| pattern200_list_or "|" pattern200 +| pattern200 +] + +impl_ident_tail: [ +| "}" +| name_list ":" lconstr "}" +| name_list "}" +| ":" lconstr "}" +] + +fixannot: [ +| "{" "struct" ident "}" +| "{" "wf" term ident "}" +| "{" "measure" term ident_opt term_opt "}" +| "{" "struct" name "}" +| empty +] + +term_opt: [ +| term +| empty +] + +impl_name_head: [ +| empty +] + +binders_fixannot: [ +| impl_name_head impl_ident_tail binders_fixannot +| fixannot +| binder binders_fixannot +| empty +] + +open_binders: [ +| name name_list_opt ":" lconstr +| name name_list_opt binders +| name ".." name +| closed_binder binders +] + +binders: [ +| binder_list_opt +] + +binder_list_opt: [ +| binder_list_opt binder +| empty +] + +binder: [ +| name +| closed_binder +] + +typeclass_constraint: [ +| "!" operconstr200 +| "{" name "}" ":" exclam_opt operconstr200 +| name_colon exclam_opt operconstr200 +| operconstr200 +] + +type_cstr: [ +| lconstr_opt +| ":" lconstr +| empty +] + +preident: [ +| IDENT +] + +pattern_identref: [ +| "?" ident +] + +var: [ +| ident +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +basequalid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +by_notation: [ +| ne_string IDENT_opt +] + +IDENT_opt: [ +| "%" IDENT +| empty +] + +smart_global: [ +| reference +| by_notation +] + +qualid: [ +| basequalid +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident field_list_opt +] + +field_list_opt: [ +| field_list_opt field +| empty +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| NUMERAL +| "-" NUMERAL +] + +natural: [ +| NUMERAL +] + +bigint: [ +| NUMERAL +] + +bar_cbrace: [ +| "|" "}" +] + +vernac_control: [ +| "Time" vernac_control +| "Redirect" ne_string vernac_control +| "Timeout" natural vernac_control +| "Fail" vernac_control +| decorated_vernac +] + +decorated_vernac: [ +| quoted_attributes_list_opt vernac +] + +quoted_attributes_list_opt: [ +| quoted_attributes_list_opt quoted_attributes +| empty +] + +quoted_attributes: [ +| "#[" attribute_list_comma_opt "]" +] + +attribute_list_comma_opt: [ +| attribute_list_comma +| empty +] + +attribute_list_comma: [ +| attribute_list_comma "," attribute +| attribute +] + +attribute: [ +| ident attribute_value +] + +attribute_value: [ +| "=" string +| "(" attribute_list_comma_opt ")" +| empty +] + +vernac: [ +| "Local" vernac_poly +| "Global" vernac_poly +| vernac_poly +] + +vernac_poly: [ +| "Polymorphic" vernac_aux +| "Monomorphic" vernac_aux +| vernac_aux +] + +vernac_aux: [ +| "Program" gallina "." +| "Program" gallina_ext "." +| gallina "." +| gallina_ext "." +| command "." +| syntax "." +| subprf +| command_entry +] + +noedit_mode: [ +| query_command +] + +subprf: [ +| BULLET +| "{" +| "}" +] + +gallina: [ +| thm_token ident_decl binders ":" lconstr with_list_opt +| 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" rec_definition_list +| "Let" "Fixpoint" rec_definition_list +| "CoFixpoint" corec_definition_list +| "Let" "CoFixpoint" corec_definition_list +| "Scheme" scheme_list +| "Combined" "Scheme" ident "from" ident_list_comma +| "Register" global "as" qualid +| "Register" "Inline" global +| "Primitive" ident lconstr_opt ":=" register_token +| "Universe" ident_list +| "Universes" ident_list +| "Constraint" univ_constraint_list_comma +] + +with_list_opt: [ +| with_list_opt "with" ident_decl binders ":" lconstr +| empty +] + +cumulativity_token_opt: [ +| cumulativity_token +| empty +] + +inductive_definition_list: [ +| inductive_definition_list "with" inductive_definition +| inductive_definition +] + +rec_definition_list: [ +| rec_definition_list "with" rec_definition +| rec_definition +] + +corec_definition_list: [ +| corec_definition_list "with" corec_definition +| corec_definition +] + +scheme_list: [ +| scheme_list "with" scheme +| scheme +] + +ident_list_comma: [ +| ident_list_comma "," ident +| ident +] + +univ_constraint_list_comma: [ +| univ_constraint_list_comma "," univ_constraint +| univ_constraint +] + +lconstr_opt2: [ +| ":=" lconstr +| empty +] + +register_token: [ +| register_prim_token +| register_type_token +] + +register_type_token: [ +| "#int63_type" +] + +register_prim_token: [ +| "#int63_head0" +| "#int63_tail0" +| "#int63_add" +| "#int63_sub" +| "#int63_mul" +| "#int63_div" +| "#int63_mod" +| "#int63_lsr" +| "#int63_lsl" +| "#int63_land" +| "#int63_lor" +| "#int63_lxor" +| "#int63_addc" +| "#int63_subc" +| "#int63_addcarryc" +| "#int63_subcarryc" +| "#int63_mulc" +| "#int63_diveucl" +| "#int63_div21" +| "#int63_addmuldiv" +| "#int63_eq" +| "#int63_lt" +| "#int63_le" +| "#int63_compare" +] + +thm_token: [ +| "Theorem" +| "Lemma" +| "Fact" +| "Remark" +| "Corollary" +| "Proposition" +| "Property" +] + +def_token: [ +| "Definition" +| "Example" +| "SubClass" +] + +assumption_token: [ +| "Hypothesis" +| "Variable" +| "Axiom" +| "Parameter" +| "Conjecture" +] + +assumptions_token: [ +| "Hypotheses" +| "Variables" +| "Axioms" +| "Parameters" +| "Conjectures" +] + +inline: [ +| "Inline" "(" natural ")" +| "Inline" +| empty +] + +univ_constraint: [ +| universe_name lt_alt universe_name +] + +lt_alt: [ +| "<" +| "=" +| "<=" +] + +univ_decl: [ +| "@{" ident_list_opt plus_opt univ_constraint_alt +] + +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: [ +| "}" +| bar_cbrace +] + +ident_decl: [ +| ident univ_decl_opt +] + +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" +] + +cumulativity_token: [ +| "Cumulative" +| "NonCumulative" +] + +private_token: [ +| "Private" +| empty +] + +def_body: [ +| binders ":=" reduce lconstr +| binders ":" lconstr ":=" reduce lconstr +| binders ":" lconstr +] + +reduce: [ +| "Eval" red_expr "in" +| empty +] + +one_decl_notation: [ +| ne_lstring ":=" term IDENT_opt2 +] + +IDENT_opt2: [ +| ":" IDENT +| empty +] + +decl_sep: [ +| "and" +] + +decl_notation: [ +| "where" one_decl_notation_list +| empty +] + +one_decl_notation_list: [ +| one_decl_notation_list decl_sep one_decl_notation +| one_decl_notation +] + +opt_constructors_or_fields: [ +| ":=" constructor_list_or_record_decl +| empty +] + +inductive_definition: [ +| opt_coercion ident_decl binders lconstr_opt opt_constructors_or_fields decl_notation +] + +constructor_list_or_record_decl: [ +| "|" constructor_list_or +| ident constructor_type "|" constructor_list_or_opt +| 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 +] + +opt_coercion: [ +| ">" +| empty +] + +rec_definition: [ +| ident_decl binders_fixannot type_cstr lconstr_opt2 decl_notation +] + +corec_definition: [ +| ident_decl binders type_cstr lconstr_opt2 decl_notation +] + +lconstr_opt: [ +| ":" lconstr +| empty +] + +scheme: [ +| scheme_kind +| ident ":=" scheme_kind +] + +scheme_kind: [ +| "Induction" "for" smart_global "Sort" sort_family +| "Minimality" "for" smart_global "Sort" sort_family +| "Elimination" "for" smart_global "Sort" sort_family +| "Case" "for" smart_global "Sort" sort_family +| "Equality" "for" smart_global +] + +record_field: [ +| quoted_attributes_list_opt record_binder natural_opt2 decl_notation +] + +record_binder_body: [ +| binders of_type_with_opt_coercion lconstr +| binders of_type_with_opt_coercion lconstr ":=" lconstr +| binders ":=" lconstr +] + +record_binder: [ +| name +| name record_binder_body +] + +assum_list: [ +| assum_coe_list +| 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 lconstr +] + +ident_decl_list: [ +| ident_decl_list ident_decl +| ident_decl +] + +constructor_type: [ +| binders of_type_with_opt_coercion_opt +] + +of_type_with_opt_coercion_opt: [ +| of_type_with_opt_coercion lconstr +| empty +] + +constructor: [ +| ident constructor_type +] + +of_type_with_opt_coercion: [ +| ":>>" +| ":>" ">" +| ":>" +| ":" ">" ">" +| ":" ">" +| ":" +] + +gallina_ext: [ +| "Module" export_token ident module_binder_list_opt of_module_type is_module_expr +| "Module" "Type" ident module_binder_list_opt check_module_types is_module_type +| "Declare" "Module" export_token ident module_binder_list_opt ":" module_type_inl +| "Section" ident +| "Chapter" ident +| "End" ident +| "Collection" ident ":=" section_subset_expr +| "Require" export_token global_list +| "From" global "Require" export_token global_list +| "Import" global_list +| "Export" global_list +| "Include" module_type_inl ext_module_expr_list_opt +| "Include" "Type" module_type_inl ext_module_type_list_opt +| "Transparent" smart_global_list +| "Opaque" smart_global_list +| "Strategy" strategy_level_list +| "Canonical" Structure_opt global univ_decl_opt2 +| "Canonical" Structure_opt by_notation +| "Coercion" global univ_decl_opt def_body +| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr +| "Coercion" global ":" class_rawexpr ">->" class_rawexpr +| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Context" binder_list +| "Instance" instance_name ":" operconstr200 hint_info record_declaration_opt +| "Existing" "Instance" global hint_info +| "Existing" "Instances" global_list natural_opt2 +| "Existing" "Class" global +| "Arguments" smart_global argument_spec_block_list_opt more_implicits_block_opt arguments_modifier_opt +| "Implicit" "Type" reserv_list +| "Implicit" "Types" reserv_list +| "Generalizable" All_alt +| "Export" "Set" option_table option_setting +| "Export" "Unset" option_table +| "Import" "Prenex" "Implicits" (* ssr plugin *) +] + +module_binder_list_opt: [ +| module_binder_list_opt module_binder +| empty +] + +ext_module_expr_list_opt: [ +| ext_module_expr_list_opt ext_module_expr +| empty +] + +ext_module_type_list_opt: [ +| ext_module_type_list_opt ext_module_type +| empty +] + +strategy_level_list: [ +| strategy_level_list strategy_level "[" smart_global_list "]" +| strategy_level "[" smart_global_list "]" +] + +Structure_opt: [ +| "Structure" +| empty +] + +univ_decl_opt: [ +| univ_decl +| empty +] + +binder_list: [ +| binder_list binder +| binder +] + +record_declaration_opt: [ +| ":=" "{" record_declaration "}" +| ":=" lconstr +| empty +] + +natural_opt: [ +| natural +| 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 +] + +export_token: [ +| "Import" +| "Export" +| empty +] + +ext_module_type: [ +| "<+" module_type_inl +] + +ext_module_expr: [ +| "<+" module_expr_inl +] + +check_module_type: [ +| "<:" module_type_inl +] + +check_module_types: [ +| check_module_type_list_opt +] + +check_module_type_list_opt: [ +| check_module_type_list_opt check_module_type +| empty +] + +of_module_type: [ +| ":" module_type_inl +| check_module_types +] + +is_module_type: [ +| ":=" module_type_inl ext_module_type_list_opt +| empty +] + +is_module_expr: [ +| ":=" module_expr_inl ext_module_expr_list_opt +| empty +] + +functor_app_annot: [ +| "[" "inline" "at" "level" natural "]" +| "[" "no" "inline" "]" +| empty +] + +module_expr_inl: [ +| "!" module_expr +| module_expr functor_app_annot +] + +module_type_inl: [ +| "!" module_type +| module_type functor_app_annot +] + +module_binder: [ +| "(" export_token ident_list ":" module_type_inl ")" +] + +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom +] + +module_expr_atom: [ +| qualid +| "(" module_expr ")" +] + +with_declaration: [ +| "Definition" fullyqualid univ_decl_opt ":=" lconstr +| "Module" fullyqualid ":=" qualid +] + +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration +] + +section_subset_expr: [ +| starredidentref_list_opt +| ssexpr35 +] + +starredidentref_list_opt: [ +| starredidentref_list_opt starredidentref +| empty +] + +starredidentref: [ +| ident +| ident "*" +| "Type" +| "Type" "*" +] + +ssexpr35: [ +| "-" ssexpr50 +| ssexpr50 +] + +ssexpr50: [ +| ssexpr0 "-" ssexpr0 +| ssexpr0 "+" ssexpr0 +| ssexpr0 +] + +ssexpr0: [ +| starredidentref +| "(" starredidentref_list_opt ")" +| "(" starredidentref_list_opt ")" "*" +| "(" ssexpr35 ")" +| "(" ssexpr35 ")" "*" +] + +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" +] + +scope: [ +| "%" IDENT +] + +argument_spec: [ +| exclam_opt name scope_opt +] + +exclam_opt: [ +| "!" +| empty +] + +scope_opt: [ +| scope +| empty +] + +argument_spec_block: [ +| argument_spec +| "/" +| "&" +| "(" argument_spec_list ")" scope_opt +| "[" argument_spec_list "]" scope_opt +| "{" argument_spec_list "}" scope_opt +] + +argument_spec_list: [ +| argument_spec_list argument_spec +| argument_spec +] + +more_implicits_block: [ +| name +| "[" name_list "]" +| "{" name_list "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +instance_name: [ +| ident_decl binders +| empty +] + +hint_info: [ +| "|" natural_opt constr_pattern_opt +| empty +] + +reserv_list: [ +| reserv_tuple_list +| simple_reserv +] + +reserv_tuple_list: [ +| reserv_tuple_list reserv_tuple +| reserv_tuple +] + +reserv_tuple: [ +| "(" simple_reserv ")" +] + +simple_reserv: [ +| ident_list ":" lconstr +] + +command: [ +| "Comments" comment_list_opt +| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Scope" IDENT +| "Pwd" +| "Cd" +| "Cd" ne_string +| "Load" Verbose_opt ne_string_alt +| "Declare" "ML" "Module" ne_string_list +| "Locate" locatable +| "Add" "LoadPath" ne_string as_dirpath +| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Remove" "LoadPath" ne_string +| "AddPath" ne_string "as" as_dirpath +| "AddRecPath" ne_string "as" as_dirpath +| "DelPath" ne_string +| "Type" lconstr +| "Print" printable +| "Print" smart_global univ_name_list_opt +| "Print" "Module" "Type" global +| "Print" "Module" global +| "Print" "Namespace" dirpath +| "Inspect" natural +| "Add" "ML" "Path" ne_string +| "Add" "Rec" "ML" "Path" ne_string +| "Set" option_table option_setting +| "Unset" option_table +| "Print" "Table" option_table +| "Add" IDENT IDENT option_ref_value_list +| "Add" IDENT option_ref_value_list +| "Test" option_table "for" option_ref_value_list +| "Test" option_table +| "Remove" IDENT IDENT option_ref_value_list +| "Remove" IDENT option_ref_value_list +| "Write" "State" IDENT +| "Write" "State" ne_string +| "Restore" "State" IDENT +| "Restore" "State" ne_string +| "Reset" "Initial" +| "Reset" ident +| "Back" +| "Back" natural +| "BackTo" natural +| "Debug" "On" +| "Debug" "Off" +| "Declare" "Reduction" IDENT; ":=" red_expr +| "Declare" "Custom" "Entry" IDENT +| "Goal" lconstr +| "Proof" +| "Proof" "Mode" string +| "Proof" lconstr +| "Abort" +| "Abort" "All" +| "Abort" ident +| "Existential" natural constr_body +| "Admitted" +| "Qed" +| "Save" ident +| "Defined" +| "Defined" ident +| "Restart" +| "Undo" +| "Undo" natural +| "Undo" "To" natural +| "Focus" +| "Focus" natural +| "Unfocus" +| "Unfocused" +| "Show" +| "Show" natural +| "Show" ident +| "Show" "Existentials" +| "Show" "Universes" +| "Show" "Conjectures" +| "Show" "Proof" +| "Show" "Intro" +| "Show" "Intros" +| "Show" "Match" reference +| "Guarded" +| "Create" "HintDb" IDENT discriminated_opt +| "Remove" "Hints" global_list opt_hintbases +| "Hint" hint opt_hintbases +| "Obligation" integer "of" ident ":" lglob withtac +| "Obligation" integer "of" ident withtac +| "Obligation" integer ":" lglob withtac +| "Obligation" integer withtac +| "Next" "Obligation" "of" ident withtac +| "Next" "Obligation" withtac +| "Solve" "Obligation" integer "of" ident "with" tactic +| "Solve" "Obligation" integer "with" tactic +| "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "with" tactic +| "Solve" "Obligations" +| "Solve" "All" "Obligations" "with" tactic +| "Solve" "All" "Obligations" +| "Admit" "Obligations" "of" ident +| "Admit" "Obligations" +| "Obligation" "Tactic" ":=" tactic +| "Show" "Obligation" "Tactic" +| "Obligations" "of" ident +| "Obligations" +| "Preterm" "of" ident +| "Preterm" +| "Hint" "Rewrite" orient term_list ":" preident_list_opt +| "Hint" "Rewrite" orient term_list "using" tactic ":" preident_list_opt +| "Hint" "Rewrite" orient term_list +| "Hint" "Rewrite" orient term_list "using" tactic +| "Derive" "Inversion_clear" ident "with" term "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" term +| "Derive" "Inversion" ident "with" term "Sort" sort_family +| "Derive" "Inversion" ident "with" term +| "Derive" "Dependent" "Inversion" ident "with" term "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" term "Sort" sort_family +| "Declare" "Left" "Step" term +| "Declare" "Right" "Step" term +| "Grab" "Existential" "Variables" +| "Unshelve" +| "Declare" "Equivalent" "Keys" term term +| "Print" "Equivalent" "Keys" +| "Optimize" "Proof" +| "Optimize" "Heap" +| "Reset" "Ltac" "Profile" +| "Show" "Ltac" "Profile" +| "Show" "Ltac" "Profile" "CutOff" int +| "Show" "Ltac" "Profile" string +| "Hint" "Cut" "[" hints_path "]" opthints +| "Typeclasses" "Transparent" reference_list_opt +| "Typeclasses" "Opaque" reference_list_opt +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy int_opt +| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "as" ident +| "Add" "Relation" term term "symmetry" "proved" "by" term "as" ident +| "Add" "Relation" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "transitivity" "proved" "by" term "as" ident +| "Add" "Setoid" term term term "as" ident +| "Add" "Parametric" "Setoid" binders ":" term term term "as" ident +| "Add" "Morphism" term ":" ident +| "Declare" "Morphism" term ":" ident +| "Add" "Morphism" term "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" binders ":" term "with" "signature" lconstr "as" ident +| "Print" "Rewrite" "HintDb" preident +| "Proof" "with" tactic using_opt +| "Proof" "using" section_subset_expr with_opt +| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" tactic +| "Print" "Ltac" reference +| "Locate" "Ltac" reference +| "Ltac" ltac_tacdef_body_list +| "Print" "Ltac" "Signatures" +| "String" "Notation" reference reference reference ":" ident +| "Set" "Firstorder" "Solver" tactic +| "Print" "Firstorder" "Solver" +| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "Derive" ident "SuchThat" term "As" ident (* derive plugin *) +| "Extraction" global (* extraction plugin *) +| "Recursive" "Extraction" global_list (* extraction plugin *) +| "Extraction" string global_list (* extraction plugin *) +| "Extraction" "TestCompile" global_list (* extraction plugin *) +| "Separate" "Extraction" global_list (* extraction plugin *) +| "Extraction" "Library" ident (* extraction plugin *) +| "Recursive" "Extraction" "Library" ident (* extraction plugin *) +| "Extraction" "Language" language (* extraction plugin *) +| "Extraction" "Inline" global_list (* extraction plugin *) +| "Extraction" "NoInline" global_list (* extraction plugin *) +| "Print" "Extraction" "Inline" (* extraction plugin *) +| "Reset" "Extraction" "Inline" (* extraction plugin *) +| "Extraction" "Implicit" global "[" int_or_id_list_opt "]" (* extraction plugin *) +| "Extraction" "Blacklist" ident_list (* extraction plugin *) +| "Print" "Extraction" "Blacklist" (* extraction plugin *) +| "Reset" "Extraction" "Blacklist" (* extraction plugin *) +| "Extract" "Constant" global string_list_opt "=>" mlname (* extraction plugin *) +| "Extract" "Inlined" "Constant" global "=>" mlname (* extraction plugin *) +| "Extract" "Inductive" global "=>" mlname "[" mlname_list_opt "]" string_opt (* extraction plugin *) +| "Show" "Extraction" (* extraction plugin *) +| "Function" function_rec_definition_loc_list (* funind plugin *) +| "Functional" "Scheme" fun_scheme_arg_list (* funind plugin *) +| "Functional" "Case" fun_scheme_arg (* funind plugin *) +| "Generate" "graph" "for" reference (* funind plugin *) +| "Add" "Ring" ident ":" term ring_mods_opt (* setoid_ring plugin *) +| "Print" "Rings" (* setoid_ring plugin *) +| "Add" "Field" ident ":" term field_mods_opt (* setoid_ring plugin *) +| "Print" "Fields" (* setoid_ring plugin *) +| "Prenex" "Implicits" global_list (* ssr plugin *) +| "Search" ssr_search_arg ssr_modlocs (* ssr plugin *) +| "Print" "Hint" "View" ssrviewpos (* ssr plugin *) +| "Hint" "View" ssrviewposspc ssrhintref_list (* ssr plugin *) +] + +comment_list_opt: [ +| comment_list_opt comment +| empty +] + +Verbose_opt: [ +| "Verbose" +| empty +] + +ne_string_alt: [ +| ne_string +| IDENT +] + +ne_string_list: [ +| ne_string_list ne_string +| ne_string +] + +univ_name_list_opt: [ +| univ_name_list +| empty +] + +option_ref_value_list: [ +| option_ref_value_list option_ref_value +| option_ref_value +] + +discriminated_opt: [ +| "discriminated" +| empty +] + +global_list: [ +| global_list global +| global +] + +preident_list_opt: [ +| preident_list_opt preident +| empty +] + +reference_list_opt: [ +| reference_list_opt reference +| empty +] + +int_opt: [ +| int +| empty +] + +using_opt: [ +| "using" section_subset_expr +| empty +] + +with_opt: [ +| "with" tactic +| empty +] + +ltac_tactic_level_opt: [ +| ltac_tactic_level +| empty +] + +ltac_production_item_list: [ +| ltac_production_item_list ltac_production_item +| ltac_production_item +] + +ltac_tacdef_body_list: [ +| ltac_tacdef_body_list "with" ltac_tacdef_body +| ltac_tacdef_body +] + +int_or_id_list_opt: [ +| int_or_id_list_opt int_or_id +| empty +] + +ident_list: [ +| ident_list ident +| ident +] + +string_list_opt: [ +| string_list_opt string +| empty +] + +mlname_list_opt: [ +| mlname_list_opt mlname +| empty +] + +string_opt: [ +| string +| empty +] + +function_rec_definition_loc_list: [ +| function_rec_definition_loc_list "with" function_rec_definition_loc +| function_rec_definition_loc +] + +fun_scheme_arg_list: [ +| fun_scheme_arg_list "with" fun_scheme_arg +| fun_scheme_arg +] + +ring_mods_opt: [ +| ring_mods +| empty +] + +field_mods_opt: [ +| field_mods +| empty +] + +ssrhintref_list: [ +| ssrhintref_list ssrhintref +| ssrhintref +] + +query_command: [ +| "Eval" red_expr "in" lconstr "." +| "Compute" lconstr "." +| "Check" lconstr "." +| "About" smart_global univ_name_list_opt "." +| "SearchHead" constr_pattern in_or_out_modules "." +| "SearchPattern" constr_pattern in_or_out_modules "." +| "SearchRewrite" constr_pattern in_or_out_modules "." +| "Search" searchabout_query searchabout_queries "." +| "SearchAbout" searchabout_query searchabout_queries "." +| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "." +] + +searchabout_query_list: [ +| searchabout_query_list searchabout_query +| searchabout_query +] + +printable: [ +| "Term" smart_global univ_name_list_opt +| "All" +| "Section" global +| "Grammar" IDENT +| "Custom" "Grammar" IDENT +| "LoadPath" dirpath_opt +| "Modules" +| "Libraries" +| "ML" "Path" +| "ML" "Modules" +| "Debug" "GC" +| "Graph" +| "Classes" +| "TypeClasses" +| "Instances" smart_global +| "Coercions" +| "Coercion" "Paths" class_rawexpr class_rawexpr +| "Canonical" "Projections" +| "Tables" +| "Options" +| "Hint" +| "Hint" smart_global +| "Hint" "*" +| "HintDb" IDENT +| "Scopes" +| "Scope" IDENT +| "Visibility" IDENT_opt3 +| "Implicit" smart_global +| Sorted_opt "Universes" printunivs_subgraph_opt ne_string_opt +| "Assumptions" smart_global +| "Opaque" "Dependencies" smart_global +| "Transparent" "Dependencies" smart_global +| "All" "Dependencies" smart_global +| "Strategy" smart_global +| "Strategies" +| "Registered" +] + +dirpath_opt: [ +| dirpath +| empty +] + +IDENT_opt3: [ +| IDENT +| empty +] + +Sorted_opt: [ +| "Sorted" +| empty +] + +printunivs_subgraph_opt: [ +| printunivs_subgraph +| empty +] + +ne_string_opt: [ +| ne_string +| empty +] + +printunivs_subgraph: [ +| "Subgraph" "(" reference_list_opt ")" +] + +class_rawexpr: [ +| "Funclass" +| "Sortclass" +| smart_global +] + +locatable: [ +| smart_global +| "Term" smart_global +| "File" ne_string +| "Library" global +| "Module" global +] + +option_setting: [ +| empty +| integer +| STRING +] + +option_ref_value: [ +| global +| STRING +] + +option_table: [ +| IDENT_list +] + +as_dirpath: [ +| as_opt3 +] + +as_opt: [ +| "as" name +| empty +] + +ne_in_or_out_modules: [ +| "inside" global_list +| "outside" global_list +] + +in_or_out_modules: [ +| ne_in_or_out_modules +| empty +] + +comment: [ +| term +| STRING +| natural +] + +positive_search_mark: [ +| "-" +| empty +] + +searchabout_query: [ +| positive_search_mark ne_string scope_opt +| positive_search_mark constr_pattern +] + +searchabout_queries: [ +| ne_in_or_out_modules +| searchabout_query searchabout_queries +| empty +] + +univ_name_list: [ +| "@{" name_list_opt "}" +] + +syntax: [ +| "Open" "Scope" IDENT +| "Close" "Scope" IDENT +| "Delimit" "Scope" IDENT; "with" IDENT +| "Undelimit" "Scope" IDENT +| "Bind" "Scope" IDENT; "with" class_rawexpr_list +| "Infix" ne_lstring ":=" term syntax_modifier_opt IDENT_opt2 +| "Notation" ident ident_list_opt ":=" term only_parsing +| "Notation" lstring ":=" term syntax_modifier_opt IDENT_opt2 +| "Format" "Notation" STRING STRING STRING +| "Reserved" "Infix" ne_lstring syntax_modifier_opt +| "Reserved" "Notation" ne_lstring 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 +] + +only_parsing: [ +| "(" "only" "parsing" ")" +| "(" "compat" STRING ")" +| empty +] + +level: [ +| "level" natural +| "next" "level" +] + +syntax_modifier: [ +| "at" "level" natural +| "in" "custom" IDENT +| "in" "custom" IDENT; "at" "level" natural +| "left" "associativity" +| "right" "associativity" +| "no" "associativity" +| "only" "printing" +| "only" "parsing" +| "compat" STRING +| "format" STRING STRING_opt +| IDENT; "," IDENT_list_comma "at" level +| IDENT; "at" level +| IDENT; "at" level constr_as_binder_kind +| IDENT constr_as_binder_kind +| IDENT syntax_extension_type +] + +STRING_opt: [ +| STRING +| empty +] + +IDENT_list_comma: [ +| IDENT_list_comma "," IDENT +| IDENT +] + +syntax_extension_type: [ +| "ident" +| "global" +| "bigint" +| "binder" +| "constr" +| "constr" at_level_opt constr_as_binder_kind_opt +| "pattern" +| "pattern" "at" "level" natural +| "strict" "pattern" +| "strict" "pattern" "at" "level" natural +| "closed" "binder" +| "custom" IDENT at_level_opt constr_as_binder_kind_opt +] + +at_level_opt: [ +| at_level +| empty +] + +constr_as_binder_kind_opt: [ +| constr_as_binder_kind +| empty +] + +at_level: [ +| "at" level +] + +constr_as_binder_kind: [ +| "as" "ident" +| "as" "pattern" +| "as" "strict" "pattern" +] + +opt_hintbases: [ +| empty +| ":" IDENT_list +] + +IDENT_list: [ +| IDENT_list IDENT +| IDENT +] + +reference_or_constr: [ +| global +| term +] + +hint: [ +| "Resolve" reference_or_constr_list hint_info +| "Resolve" "->" global_list natural_opt +| "Resolve" "<-" global_list natural_opt +| "Immediate" reference_or_constr_list +| "Variables" "Transparent" +| "Variables" "Opaque" +| "Constants" "Transparent" +| "Constants" "Opaque" +| "Transparent" global_list +| "Opaque" global_list +| "Mode" global mode +| "Unfold" global_list +| "Constructors" global_list +| "Extern" natural constr_pattern_opt "=>" tactic +] + +reference_or_constr_list: [ +| reference_or_constr_list reference_or_constr +| reference_or_constr +] + +natural_opt2: [ +| "|" natural +| empty +] + +constr_pattern_opt: [ +| constr_pattern +| empty +] + +constr_body: [ +| ":=" lconstr +| ":" lconstr ":=" lconstr +] + +mode: [ +| plus_list +] + +plus_list: [ +| plus_list plus_alt +| plus_alt +] + +plus_alt: [ +| "+" +| "!" +| "-" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "Backtrack" natural natural natural "." +| "Show" "Goal" natural "at" natural "." +| vernac_control +] + +orient: [ +| "->" +| "<-" +| empty +] + +occurrences: [ +| integer_list +| var +] + +integer_list: [ +| integer_list integer +| integer +] + +glob: [ +| term +] + +lglob: [ +| lconstr +] + +casted_constr: [ +| term +] + +hloc: [ +| empty +| "in" "|-" "*" +| "in" ident +| "in" "(" "Type" "of" ident ")" +| "in" "(" "Value" "of" ident ")" +| "in" "(" "type" "of" ident ")" +| "in" "(" "value" "of" ident ")" +] + +rename: [ +| ident "into" ident +] + +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 +] + +hypident_occ_list_comma_opt: [ +| hypident_occ_list_comma +| empty +] + +hypident_occ_list_comma: [ +| hypident_occ_list_comma "," hypident_occ +| hypident_occ +] + +test_lpar_id_colon: [ +| empty +] + +withtac: [ +| "with" tactic +| empty +] + +closed_binder: [ +| "(" name name_list ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name name_list ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name name_list "}" +| "`(" typeclass_constraint_list_comma ")" +| "`{" typeclass_constraint_list_comma "}" +| "'" pattern0 +| of_alt operconstr99 (* ssr plugin *) +| "(" "_" ":" lconstr "|" lconstr ")" +] + +typeclass_constraint_list_comma: [ +| typeclass_constraint_list_comma "," typeclass_constraint +| typeclass_constraint +] + +of_alt: [ +| "of" +| "&" +] + +simple_tactic: [ +| "reflexivity" +| "exact" casted_constr +| "assumption" +| "etransitivity" +| "cut" term +| "exact_no_check" term +| "vm_cast_no_check" term +| "native_cast_no_check" term +| "casetype" term +| "elimtype" term +| "lapply" term +| "transitivity" term +| "left" +| "eleft" +| "left" "with" bindings +| "eleft" "with" bindings +| "right" +| "eright" +| "right" "with" bindings +| "eright" "with" bindings +| "constructor" +| "constructor" int_or_var +| "constructor" int_or_var "with" bindings +| "econstructor" +| "econstructor" int_or_var +| "econstructor" int_or_var "with" bindings +| "specialize" constr_with_bindings +| "specialize" constr_with_bindings "as" simple_intropattern +| "symmetry" +| "symmetry" "in" in_clause +| "split" +| "esplit" +| "split" "with" bindings +| "esplit" "with" bindings +| "exists" +| "exists" bindings_list_comma +| "eexists" +| "eexists" bindings_list_comma +| "intros" "until" quantified_hypothesis +| "intro" +| "intro" ident +| "intro" ident "at" "top" +| "intro" ident "at" "bottom" +| "intro" ident "after" var +| "intro" ident "before" var +| "intro" "at" "top" +| "intro" "at" "bottom" +| "intro" "after" var +| "intro" "before" var +| "move" var "at" "top" +| "move" var "at" "bottom" +| "move" var "after" var +| "move" var "before" var +| "rename" rename_list_comma +| "revert" var_list +| "simple" "induction" quantified_hypothesis +| "simple" "destruct" quantified_hypothesis +| "double" "induction" quantified_hypothesis quantified_hypothesis +| "admit" +| "fix" ident natural +| "cofix" ident +| "clear" var_list_opt +| "clear" "-" var_list +| "clearbody" var_list +| "generalize" "dependent" term +| "replace" uconstr "with" term clause_dft_concl by_arg_tac +| "replace" "->" uconstr clause_dft_concl +| "replace" "<-" uconstr clause_dft_concl +| "replace" uconstr clause_dft_concl +| "simplify_eq" +| "simplify_eq" destruction_arg +| "esimplify_eq" +| "esimplify_eq" destruction_arg +| "discriminate" +| "discriminate" destruction_arg +| "ediscriminate" +| "ediscriminate" destruction_arg +| "injection" +| "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 +| "simple" "injection" +| "simple" "injection" destruction_arg +| "dependent" "rewrite" orient term +| "dependent" "rewrite" orient term "in" var +| "cutrewrite" orient term +| "cutrewrite" orient term "in" var +| "decompose" "sum" term +| "decompose" "record" term +| "absurd" term +| "contradiction" constr_with_bindings_opt +| "autorewrite" "with" preident_list clause_dft_concl +| "autorewrite" "with" preident_list clause_dft_concl "using" tactic +| "autorewrite" "*" "with" preident_list clause_dft_concl +| "autorewrite" "*" "with" preident_list clause_dft_concl "using" tactic +| "rewrite" "*" orient uconstr "in" var "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences "in" var by_arg_tac +| "rewrite" "*" orient uconstr "in" var by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr by_arg_tac +| "refine" uconstr +| "simple" "refine" uconstr +| "notypeclasses" "refine" uconstr +| "simple" "notypeclasses" "refine" uconstr +| "solve_constraints" +| "subst" var_list +| "subst" +| "simple" "subst" +| "evar" test_lpar_id_colon "(" ident ":" lconstr ")" +| "evar" term +| "instantiate" "(" ident ":=" lglob ")" +| "instantiate" "(" integer ":=" lglob ")" hloc +| "instantiate" +| "stepl" term "by" tactic +| "stepl" term +| "stepr" term "by" tactic +| "stepr" term +| "generalize_eqs" var +| "dependent" "generalize_eqs" var +| "generalize_eqs_vars" var +| "dependent" "generalize_eqs_vars" var +| "specialize_eqs" var +| "hresolve_core" "(" ident ":=" term ")" "at" int_or_var "in" term +| "hresolve_core" "(" ident ":=" term ")" "in" term +| "hget_evar" int_or_var +| "destauto" +| "destauto" "in" var +| "transparent_abstract" ltac_expr3 +| "transparent_abstract" ltac_expr3 "using" ident +| "constr_eq" term term +| "constr_eq_strict" term term +| "constr_eq_nounivs" term term +| "is_evar" term +| "has_evar" term +| "is_var" term +| "is_fix" term +| "is_cofix" term +| "is_ind" term +| "is_constructor" term +| "is_proj" term +| "is_const" term +| "shelve" +| "shelve_unifiable" +| "unshelve" ltac_expr1 +| "give_up" +| "cycle" int_or_var +| "swap" int_or_var int_or_var +| "revgoals" +| "guard" test +| "decompose" "[" term_list "]" term +| "optimize_heap" +| "start" "ltac" "profiling" +| "stop" "ltac" "profiling" +| "reset" "ltac" "profile" +| "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 +| "eassumption" +| "eexact" term +| "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" "[" uconstr_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 +| "autounfold" hintbases clause_dft_concl +| "autounfold_one" hintbases "in" var +| "autounfold_one" hintbases +| "unify" term term +| "unify" term term "with" preident +| "convert_concl_no_check" term +| "typeclasses" "eauto" "bfs" int_or_var_opt "with" preident_list +| "typeclasses" "eauto" int_or_var_opt "with" preident_list +| "typeclasses" "eauto" int_or_var_opt +| "head_of_constr" ident term +| "not_evar" term +| "is_ground" term +| "autoapply" term "using" preident +| "autoapply" term "with" preident +| "progress_evars" tactic +| "rewrite_strat" rewstrategy "in" var +| "rewrite_strat" rewstrategy +| "rewrite_db" preident "in" var +| "rewrite_db" preident +| "substitute" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings "in" var +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" var +| "setoid_rewrite" orient glob_constr_with_bindings "in" var "at" occurrences +| "setoid_symmetry" +| "setoid_symmetry" "in" var +| "setoid_reflexivity" +| "setoid_transitivity" term +| "setoid_etransitivity" +| "decide" "equality" +| "compare" term term +| "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 +| "case" induction_clause_list +| "ecase" induction_clause_list +| "fix" ident natural "with" fixdecl_list +| "cofix" ident "with" cofixdecl_list +| "pose" bindings_with_parameters +| "pose" term as_name +| "epose" bindings_with_parameters +| "epose" term as_name +| "set" bindings_with_parameters clause_dft_concl +| "set" term as_name clause_dft_concl +| "eset" bindings_with_parameters clause_dft_concl +| "eset" term as_name clause_dft_concl +| "remember" term as_name eqn_ipat clause_dft_all +| "eremember" term as_name eqn_ipat clause_dft_all +| "assert" "(" ident ":=" lconstr ")" +| "eassert" "(" ident ":=" lconstr ")" +| "assert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "eassert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "enough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "eenough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "assert" term as_ipat by_tactic +| "eassert" term as_ipat by_tactic +| "pose" "proof" lconstr as_ipat +| "epose" "proof" lconstr as_ipat +| "enough" term as_ipat by_tactic +| "eenough" term as_ipat by_tactic +| "generalize" term +| "generalize" term term_list +| "generalize" term occs as_name pattern_occ_list_opt +| "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 +| "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" term in_hyp_list +| "red" clause_dft_concl +| "hnf" clause_dft_concl +| "simpl" delta_flag ref_or_pattern_occ_opt 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" term_list clause_dft_concl +| "pattern" pattern_occ_list_comma clause_dft_concl +| "change" conversion clause_dft_concl +| "change_no_check" conversion clause_dft_concl +| "btauto" +| "rtauto" +| "congruence" +| "congruence" integer +| "congruence" "with" term_list +| "congruence" integer "with" term_list +| "f_equal" +| "firstorder" tactic_opt firstorder_using +| "firstorder" tactic_opt "with" preident_list +| "firstorder" tactic_opt firstorder_using "with" preident_list +| "gintuition" tactic_opt +| "functional" "inversion" quantified_hypothesis reference_opt (* funind plugin *) +| "functional" "induction" term_list fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" term_list fun_ind_using with_names (* funind plugin *) +| "myred" (* micromega plugin *) +| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" tactic (* micromega plugin *) +| "xlia" tactic (* micromega plugin *) +| "xnlia" tactic (* micromega plugin *) +| "xnra" tactic (* micromega plugin *) +| "xnqa" tactic (* micromega plugin *) +| "sos_Z" tactic (* micromega plugin *) +| "sos_Q" tactic (* micromega plugin *) +| "sos_R" tactic (* micromega plugin *) +| "lra_Q" tactic (* micromega plugin *) +| "lra_R" tactic (* micromega plugin *) +| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" tactic (* micromega plugin *) +| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" tactic (* micromega plugin *) +| "nsatz_compute" term (* nsatz plugin *) +| "omega" (* omega plugin *) +| "omega" "with" ident_list (* omega plugin *) +| "omega" "with" "*" (* omega plugin *) +| "protect_fv" string "in" ident (* setoid_ring plugin *) +| "protect_fv" string (* setoid_ring plugin *) +| "ring_lookup" ltac_expr0 "[" term_list_opt "]" term_list (* setoid_ring plugin *) +| "field_lookup" tactic "[" term_list_opt "]" term_list (* setoid_ring plugin *) +| "YouShouldNotTypeThis" ssrintrosarg (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +| "YouShouldNotTypeThis" "do" (* ssr plugin *) +| "YouShouldNotTypeThis" ssrtclarg ssrseqarg (* ssr plugin *) +| "clear" natural (* ssr plugin *) +| "move" ssrmovearg ssrrpat (* ssr plugin *) +| "move" ssrmovearg ssrclauses (* ssr plugin *) +| "move" ssrrpat (* ssr plugin *) +| "move" (* ssr plugin *) +| "case" ssrcasearg ssrclauses (* ssr plugin *) +| "case" (* ssr plugin *) +| "elim" ssrarg ssrclauses (* ssr plugin *) +| "elim" (* ssr plugin *) +| "apply" ssrapplyarg (* ssr plugin *) +| "apply" (* ssr plugin *) +| "exact" ssrexactarg (* ssr plugin *) +| "exact" (* ssr plugin *) +| "exact" "<:" lconstr (* ssr plugin *) +| "congr" ssrcongrarg (* ssr plugin *) +| "ssrinstancesofruleL2R" ssrterm (* ssr plugin *) +| "ssrinstancesofruleR2L" ssrterm (* ssr plugin *) +| "rewrite" ssrrwargs ssrclauses (* ssr plugin *) +| "unlock" ssrunlockargs ssrclauses (* ssr plugin *) +| "pose" ssrfixfwd (* ssr plugin *) +| "pose" ssrcofixfwd (* ssr plugin *) +| "pose" ssrfwdid ssrposefwd (* ssr plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| "have" ssrhavefwdwbinders (* ssr plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" ssrsufffwd (* ssr plugin *) +| "suffices" ssrsufffwd (* ssr plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "under" ssrrwarg (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* ssr plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* ssr plugin *) +| "ssrinstancesoftpat" cpattern (* ssrmatching plugin *) +] + +var_list: [ +| var_list var +| var +] + +var_list_opt: [ +| var_list_opt var +| empty +] + +constr_with_bindings_opt: [ +| constr_with_bindings +| empty +] + +int_or_var_opt: [ +| int_or_var +| empty +] + +uconstr_list_opt: [ +| uconstr_list_opt uconstr +| empty +] + +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 +] + +oriented_rewriter_list_comma: [ +| oriented_rewriter_list_comma "," oriented_rewriter +| oriented_rewriter +] + +simple_alt: [ +| "simple" "inversion" +| "inversion" +| "inversion_clear" +] + +with_opt2: [ +| "with" term +| empty +] + +tactic_opt: [ +| tactic +| empty +] + +reference_opt: [ +| reference +| empty +] + +bindings_list_comma: [ +| bindings_list_comma "," bindings +| bindings +] + +rename_list_comma: [ +| rename_list_comma "," rename +| rename +] + +orient_string: [ +| orient preident +] + +comparison: [ +| "=" +| "<" +| "<=" +| ">" +| ">=" +] + +test: [ +| int_or_var comparison int_or_var +] + +hintbases: [ +| "with" "*" +| "with" preident_list +| empty +] + +preident_list: [ +| preident_list preident +| preident +] + +auto_using: [ +| "using" uconstr_list_comma +| empty +] + +uconstr_list_comma: [ +| uconstr_list_comma "," uconstr +| uconstr +] + +hints_path_atom: [ +| global_list +| "_" +] + +hints_path: [ +| "(" hints_path ")" +| hints_path "*" +| "emp" +| "eps" +| hints_path "|" hints_path +| hints_path_atom +| hints_path hints_path +] + +opthints: [ +| ":" preident_list +| empty +] + +debug: [ +| "debug" +| empty +] + +eauto_search_strategy: [ +| "(bfs)" +| "(dfs)" +| empty +] + +glob_constr_with_bindings: [ +| constr_with_bindings +] + +rewstrategy: [ +| glob +| "<-" term +| "subterms" rewstrategy +| "subterm" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy +| "id" +| "fail" +| "refl" +| "progress" rewstrategy +| "try" rewstrategy +| "any" rewstrategy +| "repeat" rewstrategy +| rewstrategy ";" rewstrategy +| "(" rewstrategy ")" +| "choice" rewstrategy rewstrategy +| "old_hints" preident +| "hints" preident +| "terms" term_list_opt +| "eval" red_expr +| "fold" term +] + +term_list_opt: [ +| term_list_opt term +| empty +] + +int_or_var: [ +| integer +| ident +] + +nat_or_var: [ +| natural +| ident +] + +id_or_meta: [ +| ident +] + +open_constr: [ +| term +] + +uconstr: [ +| term +] + +destruction_arg: [ +| natural +| constr_with_bindings +| constr_with_bindings_arg +] + +constr_with_bindings_arg: [ +| ">" constr_with_bindings +| constr_with_bindings +] + +quantified_hypothesis: [ +| ident +| natural +] + +conversion: [ +| term +| term "with" term +| term "at" occs_nums "with" term +] + +occs_nums: [ +| nat_or_var_list +| "-" nat_or_var int_or_var_list_opt +] + +nat_or_var_list: [ +| nat_or_var_list nat_or_var +| nat_or_var +] + +int_or_var_list_opt: [ +| int_or_var_list_opt int_or_var +| empty +] + +occs: [ +| "at" occs_nums +| empty +] + +pattern_occ: [ +| term occs +] + +ref_or_pattern_occ: [ +| smart_global occs +| term occs +] + +unfold_occ: [ +| smart_global occs +] + +intropattern_list_opt: [ +| intropattern_list_opt intropattern +| empty +] + +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 +] + +intropattern_or_list_or: [ +| intropattern_or_list_or "|" intropattern_list_opt +| intropattern_list_opt +] + +simple_intropattern_list_opt: [ +| simple_intropattern_list_opt simple_intropattern +| empty +] + +equality_intropattern: [ +| "->" +| "<-" +| "[=" intropattern_list_opt "]" +] + +naming_intropattern: [ +| "?" ident +| "?" +| ident +] + +intropattern: [ +| simple_intropattern +| "*" +| "**" +] + +simple_intropattern: [ +| simple_intropattern_closed operconstr0_list_opt +] + +operconstr0_list_opt: [ +| operconstr0_list_opt "%" operconstr0 +| empty +] + +simple_intropattern_closed: [ +| or_and_intropattern +| equality_intropattern +| "_" +| naming_intropattern +] + +simple_binding: [ +| "(" ident ":=" lconstr ")" +| "(" natural ":=" lconstr ")" +] + +bindings: [ +| simple_binding_list +| term_list +] + +simple_binding_list: [ +| simple_binding_list simple_binding +| simple_binding +] + +term_list: [ +| term_list term +| term +] + +constr_with_bindings: [ +| term with_bindings +] + +with_bindings: [ +| "with" bindings +| empty +] + +red_flags: [ +| "beta" +| "iota" +| "match" +| "fix" +| "cofix" +| "zeta" +| "delta" delta_flag +] + +delta_flag: [ +| "-" "[" smart_global_list "]" +| "[" smart_global_list "]" +| empty +] + +smart_global_list: [ +| smart_global_list smart_global +| smart_global +] + +strategy_flag: [ +| red_flags_list +| delta_flag +] + +red_flags_list: [ +| red_flags_list red_flags +| red_flags +] + +red_expr: [ +| "red" +| "hnf" +| "simpl" delta_flag ref_or_pattern_occ_opt +| "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" term_list +| "pattern" pattern_occ_list_comma +| IDENT +] + +ref_or_pattern_occ_opt: [ +| ref_or_pattern_occ +| empty +] + +unfold_occ_list_comma: [ +| unfold_occ_list_comma "," unfold_occ +| unfold_occ +] + +pattern_occ_list_comma: [ +| pattern_occ_list_comma "," pattern_occ +| pattern_occ +] + +hypident: [ +| id_or_meta +| "(" "type" "of" id_or_meta ")" +| "(" "value" "of" id_or_meta ")" +| "(" "type" "of" ident ")" (* ssr plugin *) +| "(" "value" "of" ident ")" (* ssr plugin *) +] + +hypident_occ: [ +| hypident occs +] + +clause_dft_concl: [ +| "in" in_clause +| occs +| empty +] + +clause_dft_all: [ +| "in" in_clause +| empty +] + +opt_clause: [ +| "in" in_clause +| "at" occs_nums +| empty +] + +concl_occ: [ +| "*" occs +| empty +] + +in_hyp_list: [ +| "in" id_or_meta_list +| empty +] + +id_or_meta_list: [ +| id_or_meta_list id_or_meta +| id_or_meta +] + +in_hyp_as: [ +| "in" id_or_meta as_ipat +| empty +] + +simple_binder: [ +| name +| "(" name_list ":" lconstr ")" +] + +fixdecl: [ +| "(" ident simple_binder_list_opt fixannot ":" lconstr ")" +] + +cofixdecl: [ +| "(" ident simple_binder_list_opt ":" lconstr ")" +] + +bindings_with_parameters: [ +| "(" ident simple_binder_list_opt ":=" lconstr ")" +] + +simple_binder_list_opt: [ +| simple_binder_list_opt simple_binder +| empty +] + +eliminator: [ +| "using" constr_with_bindings +] + +as_ipat: [ +| "as" simple_intropattern +| empty +] + +or_and_intropattern_loc: [ +| or_and_intropattern +| ident +] + +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 +| natural "!" constr_with_bindings_arg +| natural qmark_alt constr_with_bindings_arg +| natural constr_with_bindings_arg +| constr_with_bindings_arg +] + +qmark_alt: [ +| "?" +| "?" +] + +oriented_rewriter: [ +| orient rewriter +] + +induction_clause: [ +| destruction_arg as_or_and_ipat eqn_ipat opt_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: [ +| eliminator +| empty +] + +ltac_expr: [ +| binder_tactic +| ltac_expr4 +] + +binder_tactic: [ +| "fun" input_fun_list "=>" ltac_expr +| "let" rec_opt let_clause_list "in" ltac_expr +| "info" ltac_expr +] + +input_fun_list: [ +| input_fun_list input_fun +| input_fun +] + +input_fun: [ +| "_" +| ident +] + +rec_opt: [ +| "rec" +| empty +] + +let_clause_list: [ +| let_clause_list "with" let_clause +| let_clause +] + +let_clause: [ +| ident ":=" ltac_expr +| "_" ":=" ltac_expr +| ident input_fun_list ":=" ltac_expr +] + +ltac_expr4: [ +| ltac_expr3 ";" binder_tactic +| ltac_expr3 ";" ltac_expr3 +| ltac_expr3 ";" "[" gt_opt tactic_then_gen "]" +| ltac_expr3 +| ltac_expr ";" "first" ssr_first_else (* ssr plugin *) +| ltac_expr ";" "first" ssrseqarg (* ssr plugin *) +| ltac_expr ";" "last" ssrseqarg (* ssr plugin *) +] + +gt_opt: [ +| ">" +| empty +] + +tactic_then_gen: [ +| ltac_expr_opt "|" tactic_then_gen +| ltac_expr_opt ".." or_opt ltac_expr_list2 +| ltac_expr +| empty +] + +ltac_expr_opt: [ +| ltac_expr +| empty +] + +ltac_expr_list_or2_opt: [ +| ltac_expr_list_or2 +| empty +] + +ltac_expr_list_or2: [ +| ltac_expr_list_or2 "|" ltac_expr_opt +| ltac_expr_opt +] + +ltac_expr3: [ +| "try" ltac_expr3 +| "do" int_or_var ltac_expr3 +| "timeout" int_or_var ltac_expr3 +| "time" string_opt ltac_expr3 +| "repeat" ltac_expr3 +| "progress" ltac_expr3 +| "once" ltac_expr3 +| "exactly_once" ltac_expr3 +| "infoH" ltac_expr3 +| "abstract" ltac_expr2 +| "abstract" ltac_expr2 "using" ident +| selector ltac_expr3 +| "do" ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "do" ssrortacarg ssrclauses (* ssr plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| ltac_expr2 +] + +tactic_mode: [ +| toplevel_selector_opt query_command +| toplevel_selector_opt "{" +| toplevel_selector_opt ltac_info_opt tactic ltac_use_default +| "par" ":" ltac_info_opt tactic ltac_use_default +] + +toplevel_selector_opt: [ +| toplevel_selector +| empty +] + +toplevel_selector: [ +| selector_body ":" +| "!" ":" +| "all" ":" +] + +selector: [ +| "only" selector_body ":" +] + +selector_body: [ +| range_selector_list_comma +| "[" ident "]" +] + +range_selector_list_comma: [ +| range_selector_list_comma "," range_selector +| range_selector +] + +range_selector: [ +| natural "-" natural +| natural +] + +ltac_expr2: [ +| ltac_expr1 "+" binder_tactic +| ltac_expr1 "+" ltac_expr2 +| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2 +| ltac_expr1 "||" binder_tactic +| ltac_expr1 "||" ltac_expr2 +| ltac_expr1 +] + +ltac_expr1: [ +| match_key reverse_opt "goal" "with" match_context_list "end" +| match_key ltac_expr "with" match_list "end" +| "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 +| reference tactic_arg_compat_list_opt +| ltac_expr ssrintros_ne (* ssr plugin *) +| ltac_expr0 +] + +match_key: [ +| "match" +| "lazymatch" +| "multimatch" +] + +reverse_opt: [ +| "reverse" +| empty +] + +ltac_expr_list_or_opt: [ +| ltac_expr_list_or +| empty +] + +ltac_expr_list_or: [ +| ltac_expr_list_or "|" ltac_expr +| ltac_expr +] + +match_context_list: [ +| or_opt match_context_rule_list_or +] + +match_context_rule_list_or: [ +| match_context_rule_list_or "|" match_context_rule +| match_context_rule +] + +or_opt: [ +| "|" +| empty +] + +eqn_list_or_opt: [ +| eqn_list_or +| empty +] + +eqn_list_or: [ +| eqn_list_or "|" eqn +| eqn +] + +match_context_rule: [ +| match_hyps_list_comma_opt "|-" match_pattern "=>" ltac_expr +| "[" match_hyps_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr +| "_" "=>" ltac_expr +] + +match_hyps_list_comma_opt: [ +| match_hyps_list_comma +| empty +] + +match_hyps_list_comma: [ +| match_hyps_list_comma "," match_hyps +| match_hyps +] + +match_hyps: [ +| name ":" match_pattern +| name ":=" match_pattern_opt match_pattern +] + +match_pattern: [ +| "context" ident_opt "[" lconstr_pattern "]" +| lconstr_pattern +] + +ident_opt: [ +| ident +| empty +] + +lconstr_pattern: [ +| lconstr +] + +match_pattern_opt: [ +| "[" match_pattern "]" ":" +| empty +] + +match_list: [ +| or_opt match_rule_list_or +] + +match_rule_list_or: [ +| match_rule_list_or "|" match_rule +| match_rule +] + +match_rule: [ +| match_pattern "=>" ltac_expr +| "_" "=>" ltac_expr +] + +message_token_list_opt: [ +| message_token_list_opt message_token +| empty +] + +message_token: [ +| ident +| STRING +| integer +] + +failkw: [ +| "fail" +| "gfail" +] + +tactic_arg: [ +| "eval" red_expr "in" term +| "context" ident "[" lconstr "]" +| "type" "of" term +| "fresh" fresh_id_list_opt +| "type_term" uconstr +| "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 +| "()" +] + +ltac_expr0: [ +| "(" ltac_expr ")" +| "[" ">" tactic_then_gen "]" +| tactic_atom +| ssrparentacarg (* ssr plugin *) +] + +tactic_atom: [ +| integer +| reference +| "()" +] + +constr_may_eval: [ +| "eval" red_expr "in" term +| "context" ident "[" lconstr "]" +| "type" "of" term +| term +] + +ltac_def_kind: [ +| ":=" +| "::=" +] + +tacdef_body: [ +| global input_fun_list ltac_def_kind ltac_expr +| global ltac_def_kind ltac_expr +] + +tactic: [ +| ltac_expr +] + +ltac_info_opt: [ +| ltac_info +| empty +] + +ltac_info: [ +| "Info" natural +] + +ltac_use_default: [ +| "." +| "..." +] + +ltac_tactic_level: [ +| "(" "at" "level" natural ")" +] + +ltac_production_sep: [ +| "," string +] + +ltac_production_item: [ +| string +| ident "(" ident ltac_production_sep_opt ")" +| ident +] + +ltac_production_sep_opt: [ +| ltac_production_sep +| empty +] + +ltac_tacdef_body: [ +| tacdef_body +] + +firstorder_using: [ +| "using" reference +| "using" reference "," reference_list_comma +| "using" reference reference reference_list_opt +| empty +] + +reference_list_comma: [ +| reference_list_comma "," reference +| reference +] + +numnotoption: [ +| empty +| "(" "warning" "after" bigint ")" +| "(" "abstract" "after" bigint ")" +] + +mlname: [ +| preident (* extraction plugin *) +| string (* extraction plugin *) +] + +int_or_id: [ +| preident (* extraction plugin *) +| integer (* extraction plugin *) +] + +language: [ +| "Ocaml" (* extraction plugin *) +| "OCaml" (* extraction plugin *) +| "Haskell" (* extraction plugin *) +| "Scheme" (* extraction plugin *) +| "JSON" (* extraction plugin *) +] + +fun_ind_using: [ +| "using" constr_with_bindings (* funind plugin *) +| empty (* funind plugin *) +] + +with_names: [ +| "as" simple_intropattern (* funind plugin *) +| empty (* funind plugin *) +] + +constr_comma_sequence': [ +| term "," constr_comma_sequence' (* funind plugin *) +| term (* funind plugin *) +] + +auto_using': [ +| "using" constr_comma_sequence' (* funind plugin *) +| empty (* funind plugin *) +] + +function_rec_definition_loc: [ +| rec_definition (* funind plugin *) +] + +fun_scheme_arg: [ +| ident ":=" "Induction" "for" reference "Sort" sort_family (* funind plugin *) +] + +ring_mod: [ +| "decidable" term (* setoid_ring plugin *) +| "abstract" (* setoid_ring plugin *) +| "morphism" term (* setoid_ring plugin *) +| "constants" "[" tactic "]" (* setoid_ring plugin *) +| "closed" "[" global_list "]" (* setoid_ring plugin *) +| "preprocess" "[" tactic "]" (* setoid_ring plugin *) +| "postprocess" "[" tactic "]" (* setoid_ring plugin *) +| "setoid" term term (* setoid_ring plugin *) +| "sign" term (* setoid_ring plugin *) +| "power" term "[" global_list "]" (* setoid_ring plugin *) +| "power_tac" term "[" tactic "]" (* setoid_ring plugin *) +| "div" term (* setoid_ring plugin *) +] + +ring_mods: [ +| "(" ring_mod_list_comma ")" (* setoid_ring plugin *) +] + +ring_mod_list_comma: [ +| ring_mod_list_comma "," ring_mod +| ring_mod +] + +field_mod: [ +| ring_mod (* setoid_ring plugin *) +| "completeness" term (* setoid_ring plugin *) +] + +field_mods: [ +| "(" field_mod_list_comma ")" (* setoid_ring plugin *) +] + +field_mod_list_comma: [ +| field_mod_list_comma "," field_mod +| field_mod +] + +ssrtacarg: [ +| ltac_expr (* ssr plugin *) +] + +ssrtac3arg: [ +| ltac_expr3 (* ssr plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* ssr plugin *) +] + +ssrhyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_hyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_id: [ +| ident (* ssr plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* ssr plugin *) +| "/=" (* ssr plugin *) +| "/" natural "/" natural "=" (* ssr plugin *) +| "/" natural "/" (* ssr plugin *) +| "/" natural "=" (* ssr plugin *) +| "/" natural "/=" (* ssr plugin *) +| "/" natural "/" "=" (* ssr plugin *) +| "//" natural "=" (* ssr plugin *) +| "//" (* ssr plugin *) +] + +ssrclear_ne: [ +| "{" ssrhyp_list "}" (* ssr plugin *) +] + +ssrclear: [ +| ssrclear_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrindex: [ +| int_or_var (* ssr plugin *) +] + +ssrocc: [ +| natural natural_list_opt (* ssr plugin *) +| "-" natural_list_opt (* ssr plugin *) +| "+" natural_list_opt (* ssr plugin *) +] + +natural_list_opt: [ +| natural_list_opt natural +| empty +] + +ssrmmod: [ +| "!" (* ssr plugin *) +| "?" (* ssr plugin *) +| "?" (* ssr plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* ssr plugin *) +| ssrmmod (* ssr plugin *) +] + +ssrmult: [ +| ssrmult_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* ssr plugin *) +| "{" ssrhyp_list_opt "}" (* ssr plugin *) +] + +ssrhyp_list_opt: [ +| ssrhyp_list_opt ssrhyp +| empty +] + +ssrterm: [ +| "YouShouldNotTypeThis" term (* ssr plugin *) +| term (* ssr plugin *) +] + +ast_closure_term: [ +| term (* ssr plugin *) +] + +ast_closure_lterm: [ +| lconstr (* ssr plugin *) +] + +ssrbwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| "/" term (* ssr plugin *) +| "/" term ssrbwdview (* ssr plugin *) +] + +ssrfwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| "/" ast_closure_term (* ssr plugin *) +| "/" ast_closure_term ssrfwdview (* ssr plugin *) +] + +ident_no_do: [ +| "YouShouldNotTypeThis" ident (* ssr plugin *) +| IDENT (* ssr plugin *) +] + +ssripat: [ +| "_" (* ssr plugin *) +| "*" (* ssr plugin *) +| ">" (* ssr plugin *) +| ident_no_do (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| "++" (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| ssrdocc (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +| "-" (* ssr plugin *) +| "-/" "=" (* ssr plugin *) +| "-/=" (* ssr plugin *) +| "-/" "/" (* ssr plugin *) +| "-//" (* ssr plugin *) +| "-/" integer "/" (* ssr plugin *) +| "-/" "/=" (* ssr plugin *) +| "-//" "=" (* ssr plugin *) +| "-//=" (* ssr plugin *) +| "-/" integer "/=" (* ssr plugin *) +| "-/" integer "/" integer "=" (* ssr plugin *) +| ssrfwdview (* ssr plugin *) +| "[" ":" ident_list_opt "]" (* ssr plugin *) +| "[:" ident_list_opt "]" (* ssr plugin *) +| ssrcpat (* ssr plugin *) +] + +ident_list_opt: [ +| ident_list_opt ident +| empty +] + +ssripats: [ +| ssripat ssripats (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* ssr plugin *) +| ssripats "|-" ">" ssriorpat (* ssr plugin *) +| ssripats "|-" ssriorpat (* ssr plugin *) +| ssripats "|->" ssriorpat (* ssr plugin *) +| ssripats "||" ssriorpat (* ssr plugin *) +| ssripats "|||" ssriorpat (* ssr plugin *) +| ssripats "||||" ssriorpat (* ssr plugin *) +| ssripats (* ssr plugin *) +] + +ssrcpat: [ +| "YouShouldNotTypeThis" ssriorpat (* ssr plugin *) +| "[" hat "]" (* ssr plugin *) +| "[" ssriorpat "]" (* ssr plugin *) +| "[=" ssriorpat "]" (* ssr plugin *) +] + +hat: [ +| "^" ident (* ssr plugin *) +| "^" "~" ident (* ssr plugin *) +| "^" "~" natural (* ssr plugin *) +| "^~" ident (* ssr plugin *) +| "^~" natural (* ssr plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* ssr plugin *) +] + +ssrhpats: [ +| ssripats (* ssr plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* ssr plugin *) +| ssripats "@" ssripats (* ssr plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* ssr plugin *) +] + +ssrrpat: [ +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* ssr plugin *) +] + +ssrintros: [ +| ssrintros_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrintrosarg: [ +| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne (* ssr plugin *) +] + +ssrfwdid: [ +| ident (* ssr plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* ssr plugin *) +| ssrtacarg "|" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +| "|" ssrortacs (* ssr plugin *) +| "|" (* ssr plugin *) +] + +ssrhintarg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtac3arg (* ssr plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* ssr plugin *) +] + +ssrhint: [ +| empty (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* ssr plugin *) +| ssrhoi_hyp (* ssr plugin *) +| "@" ssrhoi_hyp (* ssr plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" ssrhoi_id ")" (* ssr plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* ssr plugin *) +| ssrwgen ssrclausehyps (* ssr plugin *) +| ssrwgen (* ssr plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* ssr plugin *) +| "in" ssrclausehyps "|-" (* ssr plugin *) +| "in" ssrclausehyps "*" (* ssr plugin *) +| "in" ssrclausehyps (* ssr plugin *) +| "in" "|-" "*" (* ssr plugin *) +| "in" "*" (* ssr plugin *) +| "in" "*" "|-" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrbvar: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +] + +ssrbinder: [ +| ssrbvar (* ssr plugin *) +| "(" ssrbvar ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ssrbvar_list ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":=" lconstr ")" (* ssr plugin *) +| of_alt operconstr99 (* ssr plugin *) +] + +ssrbvar_list: [ +| ssrbvar_list ssrbvar +| ssrbvar +] + +ssrstruct: [ +| "{" "struct" ident "}" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrposefwd: [ +| ssrbinder_list_opt ssrfwd (* ssr plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar ssrbinder_list_opt ssrstruct ssrfwd (* ssr plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar ssrbinder_list_opt ssrfwd (* ssr plugin *) +] + +ssrbinder_list_opt: [ +| ssrbinder_list_opt ssrbinder +| empty +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* ssr plugin *) +| ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":=" lcpattern (* ssr plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" (* ssr plugin *) +| ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp ssrbinder_list_opt ssrhavefwd (* ssr plugin *) +] + +ssrseqarg: [ +| ssrswap (* ssr plugin *) +| ssrseqidx ssrortacarg ssrorelse_opt (* ssr plugin *) +| ssrseqidx ssrswap (* ssr plugin *) +| ltac_expr3 (* ssr plugin *) +] + +ssrorelse_opt: [ +| ssrorelse +| empty +] + +ssrseqidx: [ +| ident (* ssr plugin *) +| natural (* ssr plugin *) +] + +ssrswap: [ +| "first" (* ssr plugin *) +| "last" (* ssr plugin *) +] + +ssrorelse: [ +| "||" ltac_expr2 (* ssr plugin *) +] + +ident: [ +| IDENT +] + +ssrparentacarg: [ +| "(" ltac_expr ")" (* ssr plugin *) +] + +ssrdotac: [ +| ltac_expr3 (* ssr plugin *) +| ssrortacarg (* ssr plugin *) +] + +ssr_first: [ +| ssr_first ssrintros_ne (* ssr plugin *) +| "[" ltac_expr_list_or_opt "]" (* ssr plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* ssr plugin *) +| ssr_first (* ssr plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* ssr plugin *) +| cpattern (* ssr plugin *) +] + +ssrdgens_tl: [ +| "{" ssrhyp_list "}" cpattern ssrdgens_tl (* ssr plugin *) +| "{" ssrhyp_list "}" (* ssr plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* ssr plugin *) +| "/" ssrdgens_tl (* ssr plugin *) +| cpattern ssrdgens_tl (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* ssr plugin *) +] + +ssreqid: [ +| ssreqpat (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssreqpat: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrfwdview ssrclear ssrintros (* ssr plugin *) +| ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +] + +ssrmovearg: [ +| ssrarg (* ssr plugin *) +] + +ssrcasearg: [ +| ssrarg (* ssr plugin *) +] + +ssragen: [ +| "{" ssrhyp_list "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrhyp_list: [ +| ssrhyp_list ssrhyp +| ssrhyp +] + +ssragens: [ +| "{" ssrhyp_list "}" ssrterm ssragens (* ssr plugin *) +| "{" ssrhyp_list "}" (* ssr plugin *) +| ssrterm ssragens (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrbwdview ssrclear ssrintros (* ssr plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* ssr plugin *) +| ssrbwdview ssrclear (* ssr plugin *) +| ssrclear_ne (* ssr plugin *) +] + +ssrcongrarg: [ +| natural term ssrdgens (* ssr plugin *) +| natural term (* ssr plugin *) +| term ssrdgens (* ssr plugin *) +| term (* ssr plugin *) +] + +ssrrwocc: [ +| "{" ssrhyp_list_opt "}" (* ssr plugin *) +| "{" ssrocc "}" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrrule_ne: [ +| ssrterm_alt (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +] + +ssrterm_alt: [ +| "/" ssrterm +| ssrterm +| ssrsimpl_ne +] + +ssrrule: [ +| ssrrule_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "-/" ssrterm (* ssr plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" ssrhyp_list "}" ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| "{" ssrhyp_list "}" ssrrule (* ssr plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| ssrrule_ne (* ssr plugin *) +] + +ssrrwargs: [ +| ssrrwarg_list (* ssr plugin *) +] + +ssrrwarg_list: [ +| ssrrwarg_list ssrrwarg +| ssrrwarg +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrunlockargs: [ +| ssrunlockarg_list_opt (* ssr plugin *) +] + +ssrunlockarg_list_opt: [ +| ssrunlockarg_list_opt ssrunlockarg +| empty +] + +ssrsufffwd: [ +| ssrhpats ssrbinder_list_opt ":" ast_closure_lterm ssrhint (* ssr plugin *) +] + +ssrwlogfwd: [ +| ":" ssrwgen_list_opt "/" ast_closure_lterm (* ssr plugin *) +] + +ssrwgen_list_opt: [ +| ssrwgen_list_opt ssrwgen +| empty +] + +ssr_idcomma: [ +| empty (* ssr plugin *) +| IDENT_alt "," (* ssr plugin *) +] + +IDENT_alt: [ +| IDENT +| "_" +] + +ssr_rtype: [ +| "return" operconstr100 (* ssr plugin *) +] + +ssr_mpat: [ +| pattern200 (* ssr plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* ssr plugin *) +| ssr_mpat ssr_rtype (* ssr plugin *) +| ssr_mpat (* ssr plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* ssr plugin *) +] + +ssr_elsepat: [ +| "else" (* ssr plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* ssr plugin *) +] + +ssr_search_item: [ +| string (* ssr plugin *) +| string "%" preident (* ssr plugin *) +| constr_pattern (* ssr plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* ssr plugin *) +| ssr_search_item ssr_search_arg (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssr_modlocs: [ +| empty (* ssr plugin *) +| "in" modloc_list (* ssr plugin *) +] + +modloc_list: [ +| modloc_list modloc +| modloc +] + +modloc: [ +| "-" global (* ssr plugin *) +| global (* ssr plugin *) +] + +ssrhintref: [ +| term (* ssr plugin *) +| term "|" natural (* ssr plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* ssr plugin *) +| "for" "apply" "/" (* ssr plugin *) +| "for" "apply" "/" "/" (* ssr plugin *) +| "for" "apply" "//" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* ssr plugin *) +] + +rpattern: [ +| lconstr (* ssrmatching plugin *) +| "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr (* ssrmatching plugin *) +| "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "as" lconstr "in" lconstr (* ssrmatching plugin *) +] + +cpattern: [ +| "Qed" term (* ssrmatching plugin *) +| term (* ssrmatching plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* ssrmatching plugin *) +| lconstr (* ssrmatching plugin *) +] + +ssrpatternarg: [ +| rpattern (* ssrmatching plugin *) +] + +empty: [ +| +] + +lpar_id_coloneq: [ +| "(" IDENT; ":=" +] + +name_colon: [ +| IDENT; ":" +| "_" ":" +] + +int: [ +| integer +] + +command_entry: [ +| noedit_mode +] + |