(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* " tactic ] (* todo: does ARGUMENT EXTEND make the symbol global? It is in both extraargs and extratactics *) strategy_level_or_var: [ | DELETE EXTRAARGS_strategy_level | strategy_level ] operconstr0: [ | "ltac" ":" "(" tactic_expr5 ")" ] EXTRAARGS_natural: [ | DELETENT ] EXTRAARGS_lconstr: [ | DELETENT ] EXTRAARGS_strategy_level: [ | DELETENT ] G_LTAC_hint: [ | DELETENT ] G_LTAC_operconstr0: [ | DELETENT ] G_REWRITE_binders: [ | DELETE Pcoq.Constr.binders | binders ] G_TACTIC_in_clause: [ | in_clause | MOVEALLBUT in_clause | in_clause ] SPLICE: [ | G_REWRITE_binders | G_TACTIC_in_clause ] RENAME: [ | G_LTAC2_delta_flag ltac2_delta_flag | G_LTAC2_strategy_flag ltac2_strategy_flag | G_LTAC2_binder ltac2_binder | G_LTAC2_branches ltac2_branches | G_LTAC2_let_clause ltac2_let_clause | G_LTAC2_tactic_atom ltac2_tactic_atom | G_LTAC2_rewriter ltac2_rewriter | G_LTAC2_constr_with_bindings ltac2_constr_with_bindings | G_LTAC2_match_rule ltac2_match_rule | G_LTAC2_match_pattern ltac2_match_pattern | G_LTAC2_intropatterns ltac2_intropatterns | G_LTAC2_simple_intropattern ltac2_simple_intropattern | G_LTAC2_simple_intropattern_closed ltac2_simple_intropattern_closed | G_LTAC2_or_and_intropattern ltac2_or_and_intropattern | G_LTAC2_equality_intropattern ltac2_equality_intropattern | G_LTAC2_naming_intropattern ltac2_naming_intropattern | G_LTAC2_destruction_arg ltac2_destruction_arg | G_LTAC2_with_bindings ltac2_with_bindings | G_LTAC2_bindings ltac2_bindings | G_LTAC2_simple_binding ltac2_simple_binding | G_LTAC2_in_clause ltac2_in_clause | G_LTAC2_occs ltac2_occs | G_LTAC2_occs_nums ltac2_occs_nums | G_LTAC2_concl_occ ltac2_concl_occ | G_LTAC2_hypident_occ ltac2_hypident_occ | G_LTAC2_hypident ltac2_hypident | G_LTAC2_induction_clause ltac2_induction_clause | G_LTAC2_as_or_and_ipat ltac2_as_or_and_ipat | G_LTAC2_eqn_ipat ltac2_eqn_ipat | G_LTAC2_conversion ltac2_conversion | G_LTAC2_oriented_rewriter ltac2_oriented_rewriter | G_LTAC2_tactic_then_gen ltac2_tactic_then_gen | G_LTAC2_tactic_then_last ltac2_tactic_then_last | G_LTAC2_as_name ltac2_as_name | G_LTAC2_as_ipat ltac2_as_ipat | G_LTAC2_by_tactic ltac2_by_tactic | G_LTAC2_match_list ltac2_match_list ] (* renames to eliminate qualified names put other renames at the end *) RENAME: [ (* map missing names for rhs *) | Constr.constr term | Constr.global global | Constr.lconstr lconstr | Constr.lconstr_pattern cpattern | G_vernac.query_command query_command | G_vernac.section_subset_expr section_subset_expr | Prim.ident ident | Prim.reference reference | Pvernac.Vernac_.main_entry vernac_control | Tactic.tactic tactic (* SSR *) (* | G_vernac.def_body def_body | Pcoq.Constr.constr term | Prim.by_notation by_notation | Prim.identref ident | Prim.natural natural *) | Vernac.rec_definition rec_definition (* todo: hmm, rename adds 1 prodn to closed_binder?? *) | Constr.closed_binder closed_binder ] (* written in OCaml *) impl_ident_head: [ | "{" ident ] lpar_id_coloneq: [ | "(" ident; ":=" ] (* lookahead symbols *) DELETE: [ | check_for_coloneq | local_test_lpar_id_colon | lookup_at_as_comma | test_only_starredidentrefs | test_bracket_ident | test_hash_ident | test_id_colon | test_lpar_id_colon | test_lpar_id_coloneq (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *) | test_lpar_id_rpar | test_lpar_idnum_coloneq | test_show_goal | test_name_colon | test_pipe_closedcurly | ensure_fixannot | test_array_opening | test_array_closing (* SSR *) (* | ssr_null_entry *) (* | ssrtermkind (* todo: rename as "test..." *) | term_annotation (* todo: rename as "test..." *) | test_idcomma | test_nohidden | test_not_ssrslashnum | test_ssr_rw_syntax | test_ssreqid | test_ssrfwdid | test_ssrseqvar | test_ssrslashnum00 | test_ssrslashnum01 | test_ssrslashnum10 | test_ssrslashnum11 | test_ident_no_do | ssrdoarg (* todo: this and the next one should be removed from the grammar? *) | ssrseqdir *) (* unused *) | constr_comma_sequence' | auto_using' | constr_may_eval ] (* ssrintrosarg: [ | DELETENT ] *) (* additional nts to be spliced *) hyp: [ | var ] tactic_then_last: [ | REPLACE "|" LIST0 ( OPT tactic_expr5 ) SEP "|" | WITH LIST0 ( "|" ( OPT tactic_expr5 ) ) ] goal_tactics: [ | LIST0 ( OPT tactic_expr5 ) SEP "|" ] tactic_then_gen: [ | DELETENT ] tactic_then_gen: [ | goal_tactics | OPT ( goal_tactics "|" ) OPT tactic_expr5 ".." OPT ( "|" goal_tactics ) ] tactic_then_last: [ | OPTINREF ] ltac2_tactic_then_last: [ | REPLACE "|" LIST0 ( OPT tac2expr6 ) SEP "|" (* Ltac2 plugin *) | WITH LIST0 ( "|" OPT tac2expr6 ) TAG Ltac2 ] ltac2_goal_tactics: [ | LIST0 ( OPT tac2expr6 ) SEP "|" TAG Ltac2 ] ltac2_tactic_then_gen: [ | DELETENT ] ltac2_tactic_then_gen: [ | ltac2_goal_tactics TAG Ltac2 | OPT ( ltac2_goal_tactics "|" ) OPT tac2expr6 ".." OPT ( "|" ltac2_goal_tactics ) TAG Ltac2 ] ltac2_tactic_then_last: [ | OPTINREF ] reference: [ | DELETENT ] reference: [ | qualid ] fullyqualid: [ | DELETENT ] fullyqualid: [ | qualid ] field_ident: [ | "." ident ] qualid: [ | DELETENT ] qualid: [ | ident LIST0 field_ident ] field: [ | DELETENT ] fields: [ | DELETENT ] dirpath: [ | REPLACE ident LIST0 field | WITH LIST0 ( ident "." ) ident ] let_type_cstr: [ | DELETE OPT [ ":" lconstr ] | type_cstr ] (* rename here because we want to use "return_type" for something else *) RENAME: [ | return_type as_return_type ] case_item: [ | REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ] | WITH operconstr100 OPT ("as" name) OPT [ "in" pattern200 ] ] binder_constr: [ | MOVETO term_forall_or_fun "forall" open_binders "," operconstr200 | MOVETO term_forall_or_fun "fun" open_binders "=>" operconstr200 | MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200 | MOVETO term_if "if" operconstr200 as_return_type "then" operconstr200 "else" operconstr200 | MOVETO term_fix "let" "fix" fix_decl "in" operconstr200 | MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200 | MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 | MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 | MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 | MOVETO term_fix "fix" fix_decls | MOVETO term_cofix "cofix" cofix_decls ] term_let: [ | REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200 | WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200 | "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200 (* Don't need to document that "( )" is equivalent to "()" *) | REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200 | WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" operconstr200 "in" operconstr200 | REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 | WITH "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200 | DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 ] atomic_constr: [ | MOVETO qualid_annotated global univ_instance | MOVETO primitive_notations NUMERAL | MOVETO primitive_notations string | MOVETO term_evar "_" | REPLACE "?" "[" ident "]" | WITH "?[" ident "]" | MOVETO term_evar "?[" ident "]" | REPLACE "?" "[" pattern_ident "]" | WITH "?[" pattern_ident "]" | MOVETO term_evar "?[" pattern_ident "]" | MOVETO term_evar pattern_ident evar_instance ] tactic_expr0: [ | REPLACE "[" ">" tactic_then_gen "]" | WITH "[>" tactic_then_gen "]" ] (* lexer token *) IDENT: [ | ident ] scope_key: [ | IDENT ] scope_name: [ | IDENT ] scope: [ | scope_name | scope_key ] scope_delimiter: [ | REPLACE "%" IDENT | WITH "%" scope_key ] type: [ | operconstr200 ] operconstr100: [ | REPLACE operconstr99 "<:" operconstr200 | WITH operconstr99 "<:" type | MOVETO term_cast operconstr99 "<:" type | REPLACE operconstr99 "<<:" operconstr200 | WITH operconstr99 "<<:" type | MOVETO term_cast operconstr99 "<<:" type | REPLACE operconstr99 ":" operconstr200 | WITH operconstr99 ":" type | MOVETO term_cast operconstr99 ":" type | MOVETO term_cast operconstr99 ":>" ] constr: [ | REPLACE "@" global univ_instance | WITH "@" qualid_annotated | MOVETO term_explicit "@" qualid_annotated ] operconstr10: [ (* Separate this LIST0 in the nonempty and the empty case *) (* The empty case is covered by constr *) | REPLACE "@" global univ_instance LIST0 operconstr9 | WITH "@" qualid_annotated LIST1 operconstr9 | REPLACE operconstr9 | WITH constr | MOVETO term_application operconstr9 LIST1 appl_arg | MOVETO term_application "@" qualid_annotated LIST1 operconstr9 (* fixme: add in as a prodn somewhere *) | MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref | DELETE dangling_pattern_extension_rule ] operconstr9: [ (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *) | DELETE ".." operconstr0 ".." ] operconstr1: [ | REPLACE operconstr0 ".(" global LIST0 appl_arg ")" | WITH operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *) | REPLACE operconstr0 "%" IDENT | WITH operconstr0 "%" scope_key | MOVETO term_scope operconstr0 "%" scope_key | MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")" | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" ] operconstr0: [ (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *) | DELETE "{" binder_constr "}" | REPLACE "{|" record_declaration bar_cbrace | WITH "{|" LIST0 field_def bar_cbrace | MOVETO term_record "{|" LIST0 field_def bar_cbrace | MOVETO term_generalizing "`{" operconstr200 "}" | MOVETO term_generalizing "`(" operconstr200 ")" | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")" | REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_instance | WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_instance ] fix_decls: [ | DELETE fix_decl | REPLACE fix_decl "with" LIST1 fix_decl SEP "with" "for" identref | WITH fix_decl OPT ( LIST1 ("with" fix_decl) "for" identref ) ] cofix_decls: [ | DELETE cofix_decl | REPLACE cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref | WITH cofix_decl OPT ( LIST1 ( "with" cofix_decl ) "for" identref ) ] fields_def: [ | REPLACE field_def ";" fields_def | WITH LIST1 field_def SEP ";" | DELETE field_def ] binders_fixannot: [ | DELETE binder binders_fixannot | DELETE fixannot | DELETE (* empty *) | LIST0 binder OPT fixannot ] binder: [ | DELETE name ] open_binders: [ | REPLACE name LIST0 name ":" lconstr | WITH LIST1 name ":" lconstr (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *) | DELETE name ".." name | REPLACE name LIST0 name binders | WITH LIST1 binder | DELETE closed_binder binders ] closed_binder: [ | name | REPLACE "(" name LIST1 name ":" lconstr ")" | WITH "(" LIST1 name ":" type ")" | DELETE "(" name ":" lconstr ")" | DELETE "(" name ":=" lconstr ")" | REPLACE "(" name ":" lconstr ":=" lconstr ")" | WITH "(" name type_cstr ":=" lconstr ")" | DELETE "{" name "}" | DELETE "{" name LIST1 name "}" | REPLACE "{" name LIST1 name ":" lconstr "}" | WITH "{" LIST1 name type_cstr "}" | DELETE "{" name ":" lconstr "}" | MOVETO implicit_binders "{" LIST1 name type_cstr "}" | DELETE "[" name "]" | DELETE "[" name LIST1 name "]" | REPLACE "[" name LIST1 name ":" lconstr "]" | WITH "[" LIST1 name type_cstr "]" | DELETE "[" name ":" lconstr "]" | MOVETO implicit_binders "[" LIST1 name type_cstr "]" | REPLACE "(" Prim.name ":" lconstr "|" lconstr ")" | WITH "(" Prim.name ":" type "|" lconstr ")" | MOVETO generalizing_binder "`(" LIST1 typeclass_constraint SEP "," ")" | MOVETO generalizing_binder "`{" LIST1 typeclass_constraint SEP "," "}" | MOVETO generalizing_binder "`[" LIST1 typeclass_constraint SEP "," "]" ] name_colon: [ | name ":" ] typeclass_constraint: [ | EDIT ADD_OPT "!" operconstr200 | REPLACE "{" name "}" ":" [ "!" | ] operconstr200 | WITH "{" name "}" ":" OPT "!" operconstr200 | REPLACE name ":" [ "!" | ] operconstr200 | WITH name ":" OPT "!" operconstr200 ] (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*) Prim.name: [ | REPLACE "_" | WITH name ] oriented_rewriter: [ | REPLACE orient_rw rewriter | WITH orient rewriter ] DELETE: [ | orient_rw ] pattern10: [ | REPLACE pattern1 LIST1 pattern1 | WITH pattern1 LIST0 pattern1 | DELETE pattern1 ] pattern1: [ | REPLACE pattern0 "%" IDENT | WITH pattern0 "%" scope_key ] pattern0: [ | REPLACE "(" pattern200 ")" | WITH "(" LIST1 pattern200 SEP "|" ")" | DELETE "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" | REPLACE "{|" record_patterns bar_cbrace | WITH "{|" LIST0 record_pattern bar_cbrace ] DELETE: [ | record_patterns ] eqn: [ | REPLACE LIST1 mult_pattern SEP "|" "=>" lconstr | WITH LIST1 [ LIST1 pattern100 SEP "," ] SEP "|" "=>" lconstr ] universe_increment: [ | OPTINREF ] evar_instance: [ | OPTINREF ] (* No constructor syntax, OPT [ "|" binders ] is not supported for Record *) record_definition: [ | opt_coercion ident_decl binders OPT [ ":" type ] OPT [ identref ] "{" record_fields "}" decl_notations ] (* No record syntax, opt_coercion not supported for Variant, := ... required *) variant_definition: [ | ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" decl_notations ] gallina: [ | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ] | DELETE assumptions_token inline assum_list | REPLACE finite_token LIST1 inductive_definition SEP "with" | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) | "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) | "Variant" variant_definition LIST0 ( "with" variant_definition ) | [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition ) | "Class" inductive_definition LIST0 ( "with" inductive_definition ) | REPLACE "Fixpoint" LIST1 rec_definition SEP "with" | WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) | REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with" | WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) | REPLACE "CoFixpoint" LIST1 corec_definition SEP "with" | WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) | REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with" | WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) | REPLACE "Scheme" LIST1 scheme SEP "with" | WITH "Scheme" scheme LIST0 ( "with" scheme ) ] finite_token: [ | DELETENT ] constructor_list_or_record_decl: [ | OPTINREF ] record_fields: [ | REPLACE record_field ";" record_fields | WITH LIST0 record_field SEP ";" | DELETE record_field | DELETE (* empty *) ] assumptions_token: [ | DELETENT ] inline: [ | REPLACE "Inline" "(" natural ")" | WITH "Inline" OPT ( "(" natural ")" ) | DELETE "Inline" | OPTINREF ] univ_instance: [ | OPTINREF ] univ_decl: [ | REPLACE "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] | WITH "@{" LIST0 identref OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] of_type_with_opt_coercion: [ | DELETENT ] of_type_with_opt_coercion: [ | [ ":" | ":>" | ":>>" ] type ] attribute_value: [ | OPTINREF ] def_body: [ | DELETE binders ":=" reduce lconstr | REPLACE binders ":" lconstr ":=" reduce lconstr | WITH LIST0 binder OPT (":" type) ":=" reduce lconstr | REPLACE binders ":" lconstr | WITH LIST0 binder ":" type ] reduce: [ | OPTINREF ] occs: [ | OPTINREF ] delta_flag: [ | REPLACE "-" "[" LIST1 smart_global "]" | WITH OPT "-" "[" LIST1 smart_global "]" | DELETE "[" LIST1 smart_global "]" | OPTINREF ] ltac2_delta_flag: [ | EDIT ADD_OPT "-" "[" refglobals "]" (* Ltac2 plugin *) ] ltac2_branches: [ | EDIT ADD_OPT "|" LIST1 branch SEP "|" (* Ltac2 plugin *) | OPTINREF ] RENAME: [ | red_flag ltac2_red_flag | red_flags red_flag ] RENAME: [ ] strategy_flag: [ | REPLACE OPT delta_flag | WITH delta_flag (*| REPLACE LIST1 red_flags | WITH LIST1 red_flag*) | (* empty *) | OPTINREF ] filtered_import: [ | REPLACE global "(" LIST1 one_import_filter_name SEP "," ")" | WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ] | DELETE global ] functor_app_annot: [ | OPTINREF ] is_module_expr: [ | REPLACE ":=" module_expr_inl LIST0 ext_module_expr | WITH ":=" LIST1 module_expr_inl SEP "<+" | OPTINREF ] is_module_type: [ | REPLACE ":=" module_type_inl LIST0 ext_module_type | WITH ":=" LIST1 module_type_inl SEP "<+" | OPTINREF ] gallina_ext: [ | REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] | WITH "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] | REPLACE "Implicit" "Type" reserv_list | WITH "Implicit" [ "Type" | "Types" ] reserv_list | DELETE "Implicit" "Types" reserv_list (* Per @Zimmi48, the global (qualid) must be a simple identifier if def_body is present Note that smart_global is "qualid | by_notation" and that ident_decl is "ident OPT univ_decl"; move *) | REPLACE "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ] | WITH "Canonical" OPT "Structure" ident_decl def_body | REPLACE "Canonical" OPT "Structure" by_notation | WITH "Canonical" OPT "Structure" smart_global | DELETE "Coercion" global ":" class_rawexpr ">->" class_rawexpr | REPLACE "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr | WITH "Coercion" smart_global ":" class_rawexpr ">->" class_rawexpr | REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type | WITH "Include" "Type" LIST1 module_type_inl SEP "<+" | REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] | WITH "Generalizable" [ [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ] (* don't show Export for Set, Unset *) | REPLACE "Export" "Set" option_table option_setting | WITH "Set" option_table option_setting | REPLACE "Export" "Unset" option_table | WITH "Unset" option_table | REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] | WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ] | REPLACE "From" global "Require" export_token LIST1 global | WITH "From" dirpath "Require" export_token LIST1 global ] export_token: [ | OPTINREF ] (* lexer stuff *) integer: [ | DELETENT ] RENAME: [ | integer int (* todo: review uses in .mlg files, some should be "natural" *) ] LEFTQMARK: [ | "?" ] digit: [ | "0" ".." "9" ] decnum: [ | digit LIST0 [ digit | "_" ] ] hexdigit: [ | [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ] ] hexnum: [ | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ] ] num: [ | [ decnum | hexnum ] ] natural: [ | DELETENT ] natural: [ | num (* todo: or should it be "nat"? *) ] int: [ | OPT "-" num ] numeral: [ | OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum ) | OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum ) ] bigint: [ | DELETE NUMERAL | num ] first_letter: [ | [ "a" ".." "z" | "A" ".." "Z" | "_" | unicode_letter ] ] subsequent_letter: [ | [ first_letter | digit | "'" | unicode_id_part ] ] ident: [ | DELETE IDENT | first_letter LIST0 subsequent_letter ] NUMERAL: [ | numeral ] (* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *) string: [ | DELETENT ] STRING: [ | string ] (* todo: is "bigint" useful?? *) (* todo: "check_int" in g_prim.mlg should be "check_num" *) (* added productions *) command_entry: [ | noedit_mode ] DELETE: [ | tactic_then_locality ] tactic_expr5: [ (* make these look consistent with use of binder_tactic in other tactic_expr* *) | DELETE binder_tactic | DELETE tactic_expr4 | [ tactic_expr4 | binder_tactic ] ] ltac_constructs: [ (* repeated in main ltac grammar - need to create a COPY edit *) | tactic_expr3 ";" [ tactic_expr3 | binder_tactic ] | tactic_expr3 ";" "[" tactic_then_gen "]" | tactic_expr1 "+" [ tactic_expr2 | binder_tactic ] | tactic_expr1 "||" [ tactic_expr2 | binder_tactic ] (* | qualid LIST0 tactic_arg add later due renaming tactic_arg *) | "[>" tactic_then_gen "]" | toplevel_selector tactic_expr5 ] tactic_expr4: [ | REPLACE tactic_expr3 ";" tactic_then_gen "]" | WITH tactic_expr3 ";" "[" tactic_then_gen "]" | REPLACE tactic_expr3 ";" binder_tactic | WITH tactic_expr3 ";" [ tactic_expr3 | binder_tactic ] | DELETE tactic_expr3 ";" tactic_expr3 ] l3_tactic: [ ] tactic_expr3: [ | DELETE "abstract" tactic_expr2 | REPLACE "abstract" tactic_expr2 "using" ident | WITH "abstract" tactic_expr2 OPT ( "using" ident ) | l3_tactic | MOVEALLBUT ltac_builtins | l3_tactic | tactic_expr2 ] l2_tactic: [ ] tactic_expr2: [ | REPLACE tactic_expr1 "+" binder_tactic | WITH tactic_expr1 "+" [ tactic_expr2 | binder_tactic ] | DELETE tactic_expr1 "+" tactic_expr2 | REPLACE tactic_expr1 "||" binder_tactic | WITH tactic_expr1 "||" [ tactic_expr2 | binder_tactic ] | DELETE tactic_expr1 "||" tactic_expr2 | MOVETO ltac_builtins "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2 | l2_tactic | DELETE ltac_builtins ] l1_tactic: [ ] tactic_expr1: [ | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end" | MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end" | MOVETO simple_tactic match_key tactic_expr5 "with" match_list "end" | REPLACE failkw [ int_or_var | ] LIST0 message_token | WITH failkw OPT int_or_var LIST0 message_token | REPLACE reference LIST0 tactic_arg_compat | WITH reference LIST1 tactic_arg_compat | l1_tactic | DELETE simple_tactic | MOVEALLBUT ltac_builtins | l1_tactic | tactic_arg | reference LIST1 tactic_arg_compat | tactic_expr0 ] (* split match_context_rule *) goal_pattern: [ | LIST0 match_hyps SEP "," "|-" match_pattern | "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" | "_" ] match_context_rule: [ | DELETE LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5 | DELETE "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5 | DELETE "_" "=>" tactic_expr5 | goal_pattern "=>" tactic_expr5 ] match_context_list: [ | EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|" ] match_list: [ | EDIT ADD_OPT "|" LIST1 match_rule SEP "|" ] match_rule: [ (* redundant; match_pattern -> term -> _ *) | DELETE "_" "=>" tactic_expr5 ] selector_body: [ | REPLACE range_selector_or_nth (* depends on whether range_selector_or_nth is deleted first *) | WITH LIST1 range_selector SEP "," ] range_selector_or_nth: [ | DELETENT ] firstorder_rhs: [ | firstorder_using | "with" LIST1 preident | firstorder_using "with" LIST1 preident ] where: [ | "at" "top" | "at" "bottom" | "after" ident | "before" ident ] simple_tactic: [ | DELETE "intros" | REPLACE "intros" ne_intropatterns | WITH "intros" intropatterns | DELETE "eintros" | REPLACE "eintros" ne_intropatterns | WITH "eintros" intropatterns | DELETE "autorewrite" "with" LIST1 preident clause | DELETE "autorewrite" "with" LIST1 preident clause "using" tactic | DELETE "autorewrite" "*" "with" LIST1 preident clause | REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic | WITH "autorewrite" OPT "*" "with" LIST1 preident clause OPT ( "using" tactic ) | DELETE "cofix" ident | REPLACE "cofix" ident "with" LIST1 cofixdecl | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl ) | DELETE "constructor" | DELETE "constructor" int_or_var | REPLACE "constructor" int_or_var "with" bindings | WITH "constructor" OPT int_or_var OPT ( "with" bindings ) | DELETE "econstructor" | DELETE "econstructor" int_or_var | REPLACE "econstructor" int_or_var "with" bindings | WITH "econstructor" OPT ( int_or_var OPT ( "with" bindings ) ) | DELETE "dependent" "rewrite" orient constr | REPLACE "dependent" "rewrite" orient constr "in" hyp | WITH "dependent" "rewrite" orient constr OPT ( "in" hyp ) | "firstorder" OPT tactic firstorder_rhs | DELETE "firstorder" OPT tactic firstorder_using | DELETE "firstorder" OPT tactic "with" LIST1 preident | DELETE "firstorder" OPT tactic firstorder_using "with" LIST1 preident | DELETE "fix" ident natural | REPLACE "fix" ident natural "with" LIST1 fixdecl | WITH "fix" ident natural OPT ( "with" LIST1 fixdecl ) | DELETE "generalize" constr | REPLACE "generalize" constr LIST1 constr | WITH "generalize" constr OPT ( LIST1 constr ) | EDIT "simplify_eq" ADD_OPT destruction_arg | EDIT "esimplify_eq" ADD_OPT destruction_arg | EDIT "discriminate" ADD_OPT destruction_arg | EDIT "ediscriminate" ADD_OPT destruction_arg | DELETE "injection" | DELETE "injection" destruction_arg | DELETE "injection" "as" LIST0 simple_intropattern | REPLACE "injection" destruction_arg "as" LIST0 simple_intropattern | WITH "injection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern ) | DELETE "einjection" | DELETE "einjection" destruction_arg | DELETE "einjection" "as" LIST0 simple_intropattern | REPLACE "einjection" destruction_arg "as" LIST0 simple_intropattern | WITH "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern ) | EDIT "simple" "injection" ADD_OPT destruction_arg | DELETE "intro" (* todo: change the mlg to simplify! *) | DELETE "intro" ident | DELETE "intro" ident "at" "top" | DELETE "intro" ident "at" "bottom" | DELETE "intro" ident "after" hyp | DELETE "intro" ident "before" hyp | DELETE "intro" "at" "top" | DELETE "intro" "at" "bottom" | DELETE "intro" "after" hyp | DELETE "intro" "before" hyp | "intro" OPT ident OPT where | DELETE "move" hyp "at" "top" | DELETE "move" hyp "at" "bottom" | DELETE "move" hyp "after" hyp | DELETE "move" hyp "before" hyp | "move" ident OPT where | DELETE "replace" "->" uconstr clause | DELETE "replace" "<-" uconstr clause | DELETE "replace" uconstr clause | "replace" orient uconstr clause | REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac | WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac ) | DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac | DELETE "rewrite" "*" orient uconstr "at" occurrences by_arg_tac | DELETE "rewrite" "*" orient uconstr by_arg_tac | DELETE "setoid_rewrite" orient glob_constr_with_bindings | DELETE "setoid_rewrite" orient glob_constr_with_bindings "in" hyp | DELETE "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences | REPLACE "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp | WITH "setoid_rewrite" orient glob_constr_with_bindings OPT ( "at" occurrences ) OPT ( "in" hyp ) | REPLACE "stepl" constr "by" tactic | WITH "stepl" constr OPT ( "by" tactic ) | DELETE "stepl" constr | REPLACE "stepr" constr "by" tactic | WITH "stepr" constr OPT ( "by" tactic ) | DELETE "stepr" constr | DELETE "unify" constr constr | REPLACE "unify" constr constr "with" preident | WITH "unify" constr constr OPT ( "with" preident ) | DELETE "cutrewrite" orient constr | REPLACE "cutrewrite" orient constr "in" hyp | WITH "cutrewrite" orient constr OPT ( "in" hyp ) | DELETE "destauto" | REPLACE "destauto" "in" hyp | WITH "destauto" OPT ( "in" hyp ) | REPLACE "autounfold_one" hintbases "in" hyp | WITH "autounfold_one" hintbases OPT ( "in" hyp ) | DELETE "autounfold_one" hintbases | REPLACE "rewrite_db" preident "in" hyp | WITH "rewrite_db" preident OPT ( "in" hyp ) | DELETE "rewrite_db" preident | DELETE "setoid_symmetry" | REPLACE "setoid_symmetry" "in" hyp | WITH "setoid_symmetry" OPT ( "in" hyp ) | REPLACE "rewrite_strat" rewstrategy "in" hyp | WITH "rewrite_strat" rewstrategy OPT ( "in" hyp ) | DELETE "rewrite_strat" rewstrategy | REPLACE "protect_fv" string "in" ident | WITH "protect_fv" string OPT ( "in" ident ) | DELETE "protect_fv" string | DELETE "symmetry" | REPLACE "symmetry" "in" in_clause | WITH "symmetry" OPT ( "in" in_clause ) | DELETE "split" | REPLACE "split" "with" bindings | WITH "split" OPT ( "with" bindings ) | DELETE "esplit" | REPLACE "esplit" "with" bindings | WITH "esplit" OPT ( "with" bindings ) | DELETE "specialize" constr_with_bindings | REPLACE "specialize" constr_with_bindings "as" simple_intropattern | WITH "specialize" constr_with_bindings OPT ( "as" simple_intropattern ) | DELETE "exists" | REPLACE "exists" LIST1 bindings SEP "," | WITH "exists" OPT ( LIST1 bindings SEP "," ) | DELETE "eexists" | REPLACE "eexists" LIST1 bindings SEP "," | WITH "eexists" OPT ( LIST1 bindings SEP "," ) | DELETE "left" | REPLACE "left" "with" bindings | WITH "left" OPT ( "with" bindings ) | DELETE "eleft" | REPLACE "eleft" "with" bindings | WITH "eleft" OPT ( "with" bindings ) | DELETE "right" | REPLACE "right" "with" bindings | WITH "right" OPT ( "with" bindings ) | DELETE "eright" | REPLACE "eright" "with" bindings | WITH "eright" OPT ( "with" bindings ) | DELETE "finish_timing" OPT string | REPLACE "finish_timing" "(" string ")" OPT string | WITH "finish_timing" OPT ( "(" string ")" ) OPT string | REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr | WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" int_or_var ) "in" constr | DELETE "hresolve_core" "(" ident ":=" constr ")" "in" constr | EDIT "psatz_R" ADD_OPT int_or_var tactic | EDIT "psatz_Q" ADD_OPT int_or_var tactic | EDIT "psatz_Z" ADD_OPT int_or_var tactic | REPLACE "subst" LIST1 var | WITH "subst" OPT ( LIST1 var ) | DELETE "subst" | DELETE "congruence" | DELETE "congruence" int | DELETE "congruence" "with" LIST1 constr | REPLACE "congruence" int "with" LIST1 constr | WITH "congruence" OPT int OPT ( "with" LIST1 constr ) | DELETE "show" "ltac" "profile" | REPLACE "show" "ltac" "profile" "cutoff" int | WITH "show" "ltac" "profile" OPT [ "cutoff" int | string ] | DELETE "show" "ltac" "profile" string (* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *) | DELETE "transparent_abstract" tactic3 | REPLACE "transparent_abstract" tactic3 "using" ident | WITH "transparent_abstract" tactic_expr3 OPT ( "using" ident ) ] (* todo: don't use DELETENT for this *) ne_intropatterns: [ | DELETENT ] or_and_intropattern: [ | DELETE "()" | DELETE "(" simple_intropattern ")" | REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")" | WITH "(" LIST0 simple_intropattern SEP "," ")" | EDIT "[" USE_NT intropattern_or LIST1 intropatterns SEP "|" "]" ] bar_cbrace: [ | REPLACE "|" "}" | WITH "|}" ] printable: [ | REPLACE "Scope" IDENT | WITH "Scope" scope_name | REPLACE "Visibility" OPT IDENT | WITH "Visibility" OPT scope_name | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string | DELETE "Term" smart_global OPT univ_name_list (* readded in commands *) | INSERTALL "Print" ] command: [ | REPLACE "Print" printable | WITH printable | "SubClass" ident_decl def_body | REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with" | WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body ) | REPLACE "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) | WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc ) (* funind plugin *) | REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) | WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) (* funind plugin *) | DELETE "Cd" | REPLACE "Cd" ne_string | WITH "Cd" OPT ne_string | DELETE "Back" | REPLACE "Back" natural | WITH "Back" OPT natural | REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ] | WITH "Load" OPT "Verbose" [ ne_string | IDENT ] | DELETE "Unset" option_table | REPLACE "Set" option_table option_setting | WITH OPT "Export" "Set" option_table (* set flag *) | REPLACE "Test" option_table "for" LIST1 table_value | WITH "Test" option_table OPT ( "for" LIST1 table_value ) | DELETE "Test" option_table (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Add" IDENT IDENT LIST1 table_value | WITH "Add" option_table LIST1 table_value | DELETE "Add" IDENT LIST1 table_value | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "as" ident | "Add" "Parametric" "Relation" binders ":" constr constr OPT ( "reflexivity" "proved" "by" constr ) OPT ( "symmetry" "proved" "by" constr ) OPT ("transitivity" "proved" "by" constr ) "as" ident | DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" ident | DELETE "Add" "Relation" constr constr "as" ident | DELETE "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident | DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident | DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident | DELETE "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident | "Add" "Relation" constr constr OPT ( "reflexivity" "proved" "by" constr ) OPT ( "symmetry" "proved" "by" constr ) OPT ( "transitivity" "proved" "by" constr ) "as" ident | REPLACE "Admit" "Obligations" "of" ident | WITH "Admit" "Obligations" OPT ( "of" ident ) | DELETE "Admit" "Obligations" | REPLACE "Create" "HintDb" IDENT; [ "discriminated" | ] | WITH "Create" "HintDb" IDENT; OPT "discriminated" | DELETE "Debug" "On" | REPLACE "Debug" "Off" | WITH "Debug" [ "On" | "Off" ] | EDIT "Defined" ADD_OPT identref | REPLACE "Derive" "Inversion" ident "with" constr "Sort" sort_family | WITH "Derive" "Inversion" ident "with" constr OPT ( "Sort" sort_family ) | DELETE "Derive" "Inversion" ident "with" constr | REPLACE "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family | WITH "Derive" "Inversion_clear" ident "with" constr OPT ( "Sort" sort_family ) | DELETE "Derive" "Inversion_clear" ident "with" constr | EDIT "Focus" ADD_OPT natural | DELETE "Hint" "Rewrite" orient LIST1 constr ":" LIST0 preident | REPLACE "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST0 preident | WITH "Hint" "Rewrite" orient LIST1 constr OPT ( "using" tactic ) OPT ( ":" LIST0 preident ) | DELETE "Hint" "Rewrite" orient LIST1 constr | DELETE "Hint" "Rewrite" orient LIST1 constr "using" tactic | REPLACE "Next" "Obligation" "of" ident withtac | WITH "Next" "Obligation" OPT ( "of" ident ) withtac | DELETE "Next" "Obligation" withtac | REPLACE "Obligation" int "of" ident ":" lglob withtac | WITH "Obligation" int OPT ( "of" ident ) OPT ( ":" lglob withtac ) | DELETE "Obligation" int "of" ident withtac | DELETE "Obligation" int ":" lglob withtac | DELETE "Obligation" int withtac | REPLACE "Obligations" "of" ident | WITH "Obligations" OPT ( "of" ident ) | DELETE "Obligations" | REPLACE "Preterm" "of" ident | WITH "Preterm" OPT ( "of" ident ) | DELETE "Preterm" (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Remove" IDENT IDENT LIST1 table_value | WITH "Remove" option_table LIST1 table_value | DELETE "Remove" IDENT LIST1 table_value | DELETE "Restore" "State" IDENT | DELETE "Restore" "State" ne_string | "Restore" "State" [ IDENT | ne_string ] | DELETE "Show" | DELETE "Show" natural | DELETE "Show" ident | "Show" OPT [ ident | natural ] | DELETE "Show" "Ltac" "Profile" | REPLACE "Show" "Ltac" "Profile" "CutOff" int | WITH "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ] | DELETE "Show" "Ltac" "Profile" string | DELETE "Show" "Proof" (* combined with Show Proof Diffs in vernac_toplevel *) | REPLACE "Solve" "All" "Obligations" "with" tactic | WITH "Solve" "All" "Obligations" OPT ( "with" tactic ) | DELETE "Solve" "All" "Obligations" | REPLACE "Solve" "Obligation" int "of" ident "with" tactic | WITH "Solve" "Obligation" int OPT ( "of" ident ) "with" tactic | DELETE "Solve" "Obligations" | DELETE "Solve" "Obligation" int "with" tactic | REPLACE "Solve" "Obligations" "of" ident "with" tactic | WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic ) | DELETE "Solve" "Obligations" "with" tactic | DELETE "Undo" | DELETE "Undo" natural | REPLACE "Undo" "To" natural | WITH "Undo" OPT ( OPT "To" natural ) | DELETE "Write" "State" IDENT | REPLACE "Write" "State" ne_string | WITH "Write" "State" [ IDENT | ne_string ] | DELETE "Abort" | DELETE "Abort" "All" | REPLACE "Abort" identref | WITH "Abort" OPT [ "All" | identref ] (* show the locate options as separate commands *) | DELETE "Locate" locatable | locatable | REPLACE "Print" smart_global OPT univ_name_list | WITH "Print" OPT "Term" smart_global OPT univ_name_list | REPLACE "Declare" "Scope" IDENT | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) | REPLACE "Numeral" "Notation" reference reference reference ":" ident numnotoption | WITH "Numeral" "Notation" reference reference reference ":" scope_name numnotoption | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name | DELETE "Ltac2" ltac2_entry (* was split up *) ] option_setting: [ | OPTINREF ] syntax: [ | REPLACE "Open" "Scope" IDENT | WITH "Open" "Scope" scope | REPLACE "Close" "Scope" IDENT | WITH "Close" "Scope" scope | REPLACE "Delimit" "Scope" IDENT; "with" IDENT | WITH "Delimit" "Scope" scope_name; "with" scope_key | REPLACE "Undelimit" "Scope" IDENT | WITH "Undelimit" "Scope" scope_name | REPLACE "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr | WITH "Bind" "Scope" scope_name; "with" LIST1 class_rawexpr | REPLACE "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] | WITH "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ] | REPLACE "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] | WITH "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ] ] syntax_modifier: [ | DELETE "in" "custom" IDENT | REPLACE "in" "custom" IDENT; "at" "level" natural | WITH "in" "custom" IDENT OPT ( "at" "level" natural ) | REPLACE IDENT; "," LIST1 IDENT SEP "," "at" level | WITH LIST1 IDENT SEP "," "at" level ] syntax_extension_type: [ | REPLACE "strict" "pattern" "at" "level" natural | WITH "strict" "pattern" OPT ( "at" "level" natural ) | DELETE "strict" "pattern" | DELETE "pattern" | REPLACE "pattern" "at" "level" natural | WITH "pattern" OPT ( "at" "level" natural ) | DELETE "constr" (* covered by another prod *) ] numnotoption: [ | OPTINREF ] binder_tactic: [ | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5 | MOVEALLBUT ltac_builtins ] record_binder_body: [ | REPLACE binders of_type_with_opt_coercion lconstr | WITH binders of_type_with_opt_coercion | REPLACE binders of_type_with_opt_coercion lconstr ":=" lconstr | WITH binders of_type_with_opt_coercion ":=" lconstr ] simple_assum_coe: [ | REPLACE LIST1 ident_decl of_type_with_opt_coercion lconstr | WITH LIST1 ident_decl of_type_with_opt_coercion ] constructor_type: [ | REPLACE binders [ of_type_with_opt_coercion lconstr | ] | WITH binders OPT of_type_with_opt_coercion ] (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *) (* consider tactic_command vs tac2mode *) vernac_aux: [ | tactic_mode "." ] def_token: [ | DELETE "SubClass" (* document separately from Definition and Example *) ] assumption_token: [ | REPLACE "Axiom" | WITH [ "Axiom" | "Axioms" ] | REPLACE "Conjecture" | WITH [ "Conjecture" | "Conjectures" ] | REPLACE "Hypothesis" | WITH [ "Hypothesis" | "Hypotheses" ] | REPLACE "Parameter" | WITH [ "Parameter" | "Parameters" ] | REPLACE "Variable" | WITH [ "Variable" | "Variables" ] ] attributes: [ | LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr ] legacy_attr: [ | REPLACE "Local" | WITH [ "Local" | "Global" ] | DELETE "Global" | REPLACE "Polymorphic" | WITH [ "Polymorphic" | "Monomorphic" ] | DELETE "Monomorphic" | REPLACE "Cumulative" | WITH [ "Cumulative" | "NonCumulative" ] | DELETE "NonCumulative" ] sentence: [ ] (* productions defined below *) rec_definition: [ | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations | WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] corec_definition: [ | REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations | WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] type_cstr: [ | REPLACE ":" lconstr | WITH ":" type | OPTINREF ] inductive_definition: [ | REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations | WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations ] (* note that constructor -> identref constructor_type *) constructor_list_or_record_decl: [ | DELETE "|" LIST1 constructor SEP "|" | REPLACE identref constructor_type "|" LIST1 constructor SEP "|" | WITH OPT "|" LIST1 constructor SEP "|" | DELETE identref constructor_type | REPLACE identref "{" record_fields "}" | WITH OPT identref "{" record_fields "}" | DELETE "{" record_fields "}" ] record_binder: [ | REPLACE name record_binder_body | WITH name OPT record_binder_body | DELETE name ] at_level_opt: [ | OPTINREF ] query_command: [ | REPLACE "Eval" red_expr "in" lconstr "." | WITH "Eval" red_expr "in" lconstr | REPLACE "Compute" lconstr "." | WITH "Compute" lconstr | REPLACE "Check" lconstr "." | WITH "Check" lconstr | REPLACE "About" smart_global OPT univ_name_list "." | WITH "About" smart_global OPT univ_name_list | REPLACE "SearchHead" constr_pattern in_or_out_modules "." | WITH "SearchHead" constr_pattern in_or_out_modules | REPLACE "SearchPattern" constr_pattern in_or_out_modules "." | WITH "SearchPattern" constr_pattern in_or_out_modules | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "." | WITH "SearchRewrite" constr_pattern in_or_out_modules | REPLACE "Search" search_query search_queries "." | WITH "Search" search_queries ] vernac_toplevel: [ (* note these commands can't be referenced by vernac_control commands *) | REPLACE "Drop" "." | WITH "Drop" | REPLACE "Quit" "." | WITH "Quit" | REPLACE "BackTo" natural "." | WITH "BackTo" natural | REPLACE "Show" "Goal" natural "at" natural "." | WITH "Show" "Goal" natural "at" natural | REPLACE "Show" "Proof" "Diffs" OPT "removed" "." | WITH "Show" "Proof" OPT ( "Diffs" OPT "removed" ) | DELETE vernac_control ] in_or_out_modules: [ | OPTINREF ] vernac_control: [ (* replacing vernac_control with command is cheating a little; they can't refer to the vernac_toplevel commands. cover this the descriptions of these commands *) | REPLACE "Time" vernac_control | WITH "Time" sentence | REPLACE "Redirect" ne_string vernac_control | WITH "Redirect" ne_string sentence | REPLACE "Timeout" natural vernac_control | WITH "Timeout" natural sentence | REPLACE "Fail" vernac_control | WITH "Fail" sentence | DELETE decorated_vernac ] orient: [ | OPTINREF ] in_hyp_as: [ | OPTINREF ] as_name: [ | OPTINREF ] hloc: [ | OPTINREF ] as_or_and_ipat: [ | OPTINREF ] hintbases: [ | OPTINREF ] as_ipat: [ | OPTINREF ] auto_using: [ | OPTINREF ] with_bindings: [ | OPTINREF ] eqn_ipat: [ | OPTINREF ] withtac: [ | OPTINREF ] of_module_type: [ | (* empty *) | OPTINREF ] clause_dft_all: [ | OPTINREF ] opt_clause: [ | OPTINREF ] with_names: [ | OPTINREF ] in_hyp_list: [ | OPTINREF ] struct_annot: [ | OPTINREF ] firstorder_using: [ | OPTINREF ] fun_ind_using: [ | OPTINREF ] by_arg_tac: [ | OPTINREF ] by_tactic: [ | OPTINREF ] rewriter: [ | DELETE "!" constr_with_bindings_arg | DELETE [ "?" | LEFTQMARK ] constr_with_bindings_arg | DELETE natural "!" constr_with_bindings_arg | DELETE natural [ "?" | LEFTQMARK ] constr_with_bindings_arg | DELETE natural constr_with_bindings_arg | DELETE constr_with_bindings_arg | OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg ] ltac2_rewriter: [ | DELETE "!" ltac2_constr_with_bindings (* Ltac2 plugin *) | DELETE [ "?" | LEFTQMARK ] ltac2_constr_with_bindings | DELETE lnatural "!" ltac2_constr_with_bindings (* Ltac2 plugin *) | DELETE lnatural [ "?" | LEFTQMARK ] ltac2_constr_with_bindings | DELETE lnatural ltac2_constr_with_bindings (* Ltac2 plugin *) | DELETE ltac2_constr_with_bindings (* Ltac2 plugin *) | OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings ] tac2expr0: [ | DELETE "(" ")" ] tac2type_body: [ | REPLACE ":=" tac2typ_knd (* Ltac2 plugin *) | WITH [ ":=" | "::=" ] tac2typ_knd TAG Ltac2 | DELETE "::=" tac2typ_knd (* Ltac2 plugin *) ] intropattern_or_list_or: [ (* todo: where does intropattern_or_list_or come from?? *) | REPLACE intropattern_or_list_or "|" intropatterns | WITH LIST0 intropattern LIST0 ( "|" intropatterns ) | DELETE intropatterns ] record_declaration: [ | DELETE fields_def | LIST0 field_def ] fields_def: [ | DELETENT ] hint_info: [ | OPTINREF ] debug: [ | OPTINREF ] eauto_search_strategy: [ | OPTINREF ] constr_body: [ | DELETE ":=" lconstr | REPLACE ":" lconstr ":=" lconstr | WITH OPT ( ":" lconstr ) ":=" lconstr ] opt_hintbases: [ | OPTINREF ] opthints: [ | OPTINREF ] scheme: [ | DELETE scheme_kind | REPLACE identref ":=" scheme_kind | WITH OPT ( identref ":=" ) scheme_kind ] instance_name: [ | OPTINREF ] simple_reserv: [ | REPLACE LIST1 identref ":" lconstr | WITH LIST1 identref ":" type ] in_clause: [ | DELETE in_clause' | REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ | WITH LIST0 hypident_occ SEP "," OPT ( "|-" concl_occ ) | DELETE LIST0 hypident_occ SEP "," ] ltac2_in_clause: [ | REPLACE LIST0 ltac2_hypident_occ SEP "," "|-" ltac2_concl_occ (* Ltac2 plugin *) | WITH LIST0 ltac2_hypident_occ SEP "," OPT ( "|-" ltac2_concl_occ ) TAG Ltac2 | DELETE LIST0 ltac2_hypident_occ SEP "," (* Ltac2 plugin *) ] concl_occ: [ | OPTINREF ] opt_coercion: [ | OPTINREF ] opt_constructors_or_fields: [ | OPTINREF ] decl_notations: [ | REPLACE "where" LIST1 decl_notation SEP decl_sep | WITH "where" decl_notation LIST0 (decl_sep decl_notation ) | OPTINREF ] module_expr: [ | REPLACE module_expr_atom | WITH LIST1 module_expr_atom | DELETE module_expr module_expr_atom ] locatable: [ | INSERTALL "Locate" ] ne_in_or_out_modules: [ | REPLACE "inside" LIST1 global | WITH [ "inside" | "outside" ] LIST1 global | DELETE "outside" LIST1 global ] search_queries: [ | DELETE ne_in_or_out_modules | REPLACE search_query search_queries | WITH LIST1 ( search_query ) OPT ne_in_or_out_modules | DELETE (* empty *) ] positive_search_mark: [ | OPTINREF ] SPLICE: [ | positive_search_mark ] search_query: [ | REPLACE OPT "-" search_item | WITH search_item | "-" search_query | REPLACE OPT "-" "[" LIST1 ( LIST1 search_query ) SEP "|" "]" | WITH "[" LIST1 ( LIST1 search_query ) SEP "|" "]" ] search_item: [ | REPLACE search_where ":" ne_string OPT scope_delimiter | WITH OPT ( search_where ":" ) ne_string OPT scope_delimiter | DELETE ne_string OPT scope_delimiter | REPLACE search_where ":" constr_pattern | WITH OPT ( search_where ":" ) constr_pattern | DELETE constr_pattern ] by_notation: [ | REPLACE ne_string OPT [ "%" IDENT ] | WITH ne_string OPT [ "%" scope_key ] ] decl_notation: [ | REPLACE ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] | WITH ne_lstring ":=" constr syntax_modifiers OPT [ ":" scope_name ] ] syntax_modifiers: [ | OPTINREF ] only_parsing: [ | OPTINREF ] ltac_production_item: [ | REPLACE ident "(" ident OPT ltac_production_sep ")" | WITH ident OPT ( "(" ident OPT ltac_production_sep ")" ) | DELETE ident ] input_fun: [ | DELETE ident | DELETE "_" | name ] let_clause: [ | DELETE identref ":=" tactic_expr5 | REPLACE "_" ":=" tactic_expr5 | WITH name ":=" tactic_expr5 ] tactic_mode: [ (* todo: make sure to document this production! *) (* deleting to allow splicing query_command into command *) | DELETE OPT toplevel_selector query_command | DELETE OPT ltac_selector OPT ltac_info tactic ltac_use_default | DELETE "par" ":" OPT ltac_info tactic ltac_use_default (* Ignore attributes (none apply) and "...". *) | ltac_info tactic | MOVETO command ltac_info tactic | DELETE command ] sexpr: [ | REPLACE syn_node (* Ltac2 plugin *) | WITH name TAG Ltac2 | REPLACE syn_node "(" LIST1 sexpr SEP "," ")" (* Ltac2 plugin *) | WITH name "(" LIST1 sexpr SEP "," ")" TAG Ltac2 ] syn_node: [ | DELETENT ] RENAME: [ | toplevel_selector toplevel_selector_temp ] toplevel_selector: [ | selector_body | "all" | "!" (* par is accepted even though it's not in the .mlg *) | "par" ] toplevel_selector_temp: [ | DELETE selector_body ":" | DELETE "all" ":" | DELETE "!" ":" | toplevel_selector ":" ] (* not included in insertprodn; defined in rst with :production: *) control_command: [ ] (* move all commands under "command" *) DELETE: [ | vernac ] vernac_aux: [ | DELETE gallina "." | DELETE gallina_ext "." | DELETE syntax "." | DELETE command_entry ] command: [ | gallina | gallina_ext | syntax | query_command | vernac_control | vernac_toplevel | command_entry ] SPLICE: [ | query_command ] query_command: [ ] (* re-add as a placeholder *) sentence: [ | OPT attributes command "." | OPT attributes OPT ( num ":" ) query_command "." | OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ] | control_command ] document: [ | LIST0 sentence ] (* add in ltac and Tactic Notation tactics that appear in the doc: *) ltac_defined_tactics: [ | "classical_left" | "classical_right" | "contradict" ident | "discrR" | "easy" | "exfalso" | "inversion_sigma" | "lia" | "lra" | "nia" | "nra" | "split_Rabs" | "split_Rmult" | "tauto" | "time_constr" tactic_expr5 | "zify" ] (* todo: need careful review; assume that "[" ... "]" are literals *) tactic_notation_tactics: [ | "assert_fails" tactic_expr3 | "assert_succeeds" tactic_expr3 | "field" OPT ( "[" LIST1 operconstr200 "]" ) | "field_simplify" OPT ( "[" LIST1 operconstr200 "]" ) LIST1 operconstr200 OPT ( "in" ident ) | "field_simplify_eq" OPT ( "[" LIST1 operconstr200 "]" ) OPT ( "in" ident ) | "intuition" OPT tactic_expr5 | "nsatz" OPT ( "with" "radicalmax" ":=" operconstr200 "strategy" ":=" operconstr200 "parameters" ":=" operconstr200 "variables" ":=" operconstr200 ) | "psatz" operconstr200 OPT int_or_var | "ring" OPT ( "[" LIST1 operconstr200 "]" ) | "ring_simplify" OPT ( "[" LIST1 operconstr200 "]" ) LIST1 operconstr200 OPT ( "in" ident ) (* todo: ident was "hyp", worth keeping? *) ] (* defined in OCaml outside of mlgs *) tactic_arg: [ | "uconstr" ":" "(" operconstr200 ")" | MOVEALLBUT simple_tactic ] nonterminal: [ ] value_tactic: [ ] RENAME: [ | tactic_arg tactic_value ] syn_value: [ | IDENT; ":" "(" nonterminal ")" ] tactic_value: [ | [ value_tactic | syn_value ] ] (* defined in Ltac2/Notations.v *) ltac2_match_key: [ | "lazy_match!" | "match!" | "multi_match!" ] ltac2_constructs: [ | ltac2_match_key tac2expr6 "with" ltac2_match_list "end" | ltac2_match_key OPT "reverse" "goal" "with" gmatch_list "end" ] simple_tactic: [ | ltac_builtins | ltac_constructs | ltac2_constructs | ltac_defined_tactics | tactic_notation_tactics ] tacdef_body: [ | REPLACE global LIST1 input_fun ltac_def_kind tactic_expr5 | WITH global LIST0 input_fun ltac_def_kind tactic_expr5 | DELETE global ltac_def_kind tactic_expr5 ] tac2def_typ: [ | REPLACE "Type" rec_flag LIST1 tac2typ_def SEP "with" (* Ltac2 plugin *) | WITH "Type" rec_flag tac2typ_def LIST0 ( "with" tac2typ_def ) TAG Ltac2 ] tac2def_val: [ | REPLACE mut_flag rec_flag LIST1 tac2def_body SEP "with" (* Ltac2 plugin *) | WITH mut_flag rec_flag tac2def_body LIST0 ( "with" tac2def_body ) TAG Ltac1 ] tac2alg_constructors: [ | REPLACE "|" LIST1 tac2alg_constructor SEP "|" (* Ltac2 plugin *) | WITH OPT "|" LIST1 tac2alg_constructor SEP "|" TAG Ltac2 | DELETE LIST0 tac2alg_constructor SEP "|" (* Ltac2 plugin *) | (* empty *) | OPTINREF ] SPLICE: [ | def_token | extended_def_token ] logical_kind: [ | DELETE thm_token | DELETE assumption_token | [ thm_token | assumption_token ] | DELETE "Definition" | DELETE "Example" | DELETE "Context" | DELETE "Primitive" (* SubClass was deleted from def_token *) | [ "Definition" | "Example" | "Context" | "Primitive" ] | DELETE "Coercion" | DELETE "Instance" | DELETE "Scheme" | DELETE "Canonical" | [ "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ] | DELETE "Field" | DELETE "Method" | [ "Field" | "Method" ] ] (* ltac2 *) DELETE: [ | test_ltac1_env ] mut_flag: [ | OPTINREF ] rec_flag: [ | OPTINREF ] ltac2_orient: [ | DELETENT ] ltac2_orient: [ | orient ] SPLICE: [ | ltac2_orient ] tac2typ_prm: [ | OPTINREF ] tac2type_body: [ | OPTINREF ] atomic_tac2pat: [ | OPTINREF ] tac2expr0: [ (* | DELETE "(" ")" (* covered by "()" prodn *) | REPLACE "{" [ | LIST1 tac2rec_fieldexpr OPT ";" ] "}" | WITH "{" OPT ( LIST1 tac2rec_fieldexpr OPT ";" ) "}" *) ] (* todo: should | tac2pat1 "," LIST0 tac2pat1 SEP "," use LIST1? *) SPLICE: [ | tac2expr4 ] tac2expr3: [ | REPLACE tac2expr2 "," LIST1 tac2expr2 SEP "," (* Ltac2 plugin *) | WITH LIST1 tac2expr2 SEP "," TAG Ltac2 | DELETE tac2expr2 (* Ltac2 plugin *) ] tac2rec_fieldexprs: [ | DELETE tac2rec_fieldexpr ";" tac2rec_fieldexprs | DELETE tac2rec_fieldexpr ";" | DELETE tac2rec_fieldexpr | LIST1 tac2rec_fieldexpr OPT ";" | OPTINREF ] tac2rec_fields: [ | DELETE tac2rec_field ";" tac2rec_fields | DELETE tac2rec_field ";" | DELETE tac2rec_field | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 | OPTINREF ] (* todo: weird productions, ints only after an initial "-"??: occs_nums: [ | LIST1 [ num | ident ] | "-" [ num | ident ] LIST0 int_or_var *) ltac2_occs_nums: [ | DELETE LIST1 nat_or_anti (* Ltac2 plugin *) | REPLACE "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) | WITH OPT "-" LIST1 nat_or_anti TAG Ltac2 ] syn_level: [ | OPTINREF ] ltac2_delta_flag: [ | OPTINREF ] ltac2_occs: [ | OPTINREF ] ltac2_concl_occ: [ | OPTINREF ] ltac2_with_bindings: [ | OPTINREF ] ltac2_as_or_and_ipat: [ | OPTINREF ] ltac2_eqn_ipat: [ | OPTINREF ] ltac2_as_name: [ | OPTINREF ] ltac2_as_ipat: [ | OPTINREF ] ltac2_by_tactic: [ | OPTINREF ] ltac2_entry: [ | REPLACE tac2def_typ (* Ltac2 plugin *) | WITH "Ltac2" tac2def_typ | REPLACE tac2def_syn (* Ltac2 plugin *) | WITH "Ltac2" tac2def_syn | REPLACE tac2def_mut (* Ltac2 plugin *) | WITH "Ltac2" tac2def_mut | REPLACE tac2def_val (* Ltac2 plugin *) | WITH "Ltac2" tac2def_val | REPLACE tac2def_ext (* Ltac2 plugin *) | WITH "Ltac2" tac2def_ext | "Ltac2" "Notation" [ string | lident ] ":=" tac2expr6 TAG Ltac2 (* variant *) | MOVEALLBUT command (* todo: MOVEALLBUT should ignore tag on "but" prodns *) ] ltac2_match_list: [ | EDIT ADD_OPT "|" LIST1 ltac2_match_rule SEP "|" (* Ltac2 plugin *) ] ltac2_or_and_intropattern: [ | DELETE "(" ltac2_simple_intropattern ")" (* Ltac2 plugin *) | REPLACE "(" ltac2_simple_intropattern "," LIST1 ltac2_simple_intropattern SEP "," ")" (* Ltac2 plugin *) | WITH "(" LIST1 ltac2_simple_intropattern SEP "," ")" TAG Ltac2 | REPLACE "(" ltac2_simple_intropattern "&" LIST1 ltac2_simple_intropattern SEP "&" ")" (* Ltac2 plugin *) | WITH "(" LIST1 ltac2_simple_intropattern SEP "&" ")" TAG Ltac2 ] SPLICE: [ | tac2def_val | tac2def_typ | tac2def_ext | tac2def_syn | tac2def_mut | mut_flag | rec_flag | locident | syn_level | tac2rec_fieldexprs | tac2type_body | tac2alg_constructors | tac2rec_fields | ltac2_binder | branch | anti ] tac2expr5: [ | REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" tac2expr6 (* Ltac2 plugin *) | WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" tac2expr6 TAG Ltac2 | MOVETO simple_tactic "match" tac2expr5 "with" OPT ltac2_branches "end" (* Ltac2 plugin *) | DELETE simple_tactic ] RENAME: [ | Prim.string string | Prim.integer int | Prim.qualid qualid | Prim.natural num ] gmatch_list: [ | EDIT ADD_OPT "|" LIST1 gmatch_rule SEP "|" (* Ltac2 plugin *) ] ltac2_quotations: [ ] ltac2_tactic_atom: [ | MOVETO ltac2_quotations "constr" ":" "(" lconstr ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "open_constr" ":" "(" lconstr ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "ident" ":" "(" lident ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "pattern" ":" "(" cpattern ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "reference" ":" "(" globref ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "ltac1" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) | MOVETO ltac2_quotations "ltac1val" ":" "(" ltac1_expr_in_env ")" (* Ltac2 plugin *) ] (* non-Ltac2 "clause" is really clause_dft_concl + there is an ltac2 "clause" *) ltac2_clause: [ ] clause: [ | MOVEALLBUT ltac2_clause ] clause: [ | clause_dft_concl ] q_clause: [ | REPLACE clause | WITH ltac2_clause TAG Ltac2 ] ltac2_induction_clause: [ | REPLACE ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT clause (* Ltac2 plugin *) | WITH ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause TAG Ltac2 ] SPLICE: [ | clause | noedit_mode | bigint | match_list | match_context_list | IDENT | LEFTQMARK | natural | NUMERAL | STRING | hyp | var | identref | pattern_ident | constr_eval (* splices as multiple prods *) | tactic_then_last (* todo: dependency on c.edit_mlg edit?? really useful? *) | ltac2_tactic_then_last | Prim.name | ltac_selector | Constr.ident | attribute_list | operconstr99 | operconstr90 | operconstr9 | operconstr8 | pattern200 | pattern99 | pattern90 | ne_lstring | ne_string | lstring | fullyqualid | global | reference | bar_cbrace | lconstr (* | ast_closure_term | ast_closure_lterm | ident_no_do | ssrterm | ssrtacarg | ssrtac3arg | ssrtclarg | ssrhyp | ssrhoi_hyp | ssrhoi_id | ssrindex | ssrhpats | ssrhpats_nobs | ssrfwdid | ssrmovearg | ssrcasearg | ssrrwargs | ssrviewposspc | ssrpatternarg | ssr_elsepat | ssr_mpat | ssrunlockargs | ssrcofixfwd | ssrfixfwd | ssrhavefwdwbinders | ssripats_ne | ssrparentacarg | ssrposefwd *) | preident | lpar_id_coloneq | binders | casted_constr | check_module_types | constr_pattern | decl_sep | function_rec_definition_loc (* loses funind annotation *) | glob | glob_constr_with_bindings | id_or_meta | lglob | ltac_tacdef_body | mode | mult_pattern | open_constr | record_declaration | tactic | uconstr | impl_ident_head | branches | check_module_type | decorated_vernac | ext_module_expr | ext_module_type | pattern_identref | test | binder_constr | atomic_constr | let_type_cstr | name_colon | closed_binder | binders_fixannot | as_return_type | case_type | universe_increment | type_cstr | record_pattern | evar_instance | fix_decls | cofix_decls | assum_list | assum_coe | inline | occs | ltac_info | field_mods | ltac_production_sep | ltac_tactic_level | printunivs_subgraph | ring_mods | eliminator (* todo: splice or not? *) | quoted_attributes (* todo: splice or not? *) | printable | only_parsing | record_fields | constructor_type | record_binder | at_level_opt | table_value | in_or_out_modules | option_setting | orient | with_bindings | by_arg_tac | by_tactic | quantified_hypothesis | nat_or_var | in_hyp_list | rename | export_token | reserv_tuple | inst | opt_coercion | opt_constructors_or_fields | is_module_type | is_module_expr | module_expr | mlname | withtac | debug | eauto_search_strategy | constr_body | reference_or_constr | opt_hintbases | hints_path_atom | opthints | scheme | fresh_id | ltac_def_kind | intropatterns | instance_name | failkw | selector | ne_in_or_out_modules | search_queries | locatable | scope_delimiter | bignat | one_import_filter_name | search_where | message_token | input_fun | ltac_use_default | toplevel_selector_temp | comment | register_token | match_context_rule | match_rule | by_notation | lnatural | nat_or_anti | globref | let_binder | refglobals (* Ltac2 *) | syntax_modifiers | array_elems | ltac2_expr | G_LTAC2_input_fun | ltac2_simple_intropattern_closed | ltac2_with_bindings ] (* end SPLICE *) RENAME: [ | tactic3 ltac_expr3 (* todo: can't figure out how this gets mapped by coqpp *) | tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *) | tactic0 ltac_expr0 (* todo: can't figure out how this gets mapped by coqpp *) | ltac1_expr ltac_expr | tactic_expr5 ltac_expr | tactic_expr4 ltac_expr4 | tactic_expr3 ltac_expr3 | tactic_expr2 ltac_expr2 | tactic_expr1 ltac_expr1 | tactic_expr0 ltac_expr0 (* | nonsimple_intropattern intropattern (* ltac2 *) *) | operconstr200 term (* historical name *) | operconstr100 term100 | operconstr10 term10 | operconstr1 term1 | operconstr0 term0 | pattern100 pattern | match_constr term_match (*| impl_ident_tail impl_ident*) | ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *) | tactic_then_gen for_each_goal | ltac2_tactic_then_gen ltac2_for_each_goal | selector_body selector | match_hyps match_hyp | BULLET bullet | fix_decl fix_body | cofix_decl cofix_body (* todo: it's confusing that Constr.constr and constr are different things *) | constr one_term | appl_arg arg | rec_definition fix_definition | corec_definition cofix_definition | univ_instance univ_annot | simple_assum_coe assumpt | of_type_with_opt_coercion of_type | attribute_value attr_value | constructor_list_or_record_decl constructors_or_record | record_binder_body field_body | class_rawexpr class | smart_global reference (* | searchabout_query search_item *) | option_table setting_name | argument_spec_block arg_specs | more_implicits_block implicits_alt | arguments_modifier args_modifier | constr_as_binder_kind binder_interp | syntax_extension_type explicit_subentry | numnotoption numeral_modifier | tactic_arg_compat tactic_arg | lconstr_pattern cpattern | Pltac.tactic ltac_expr | sexpr ltac2_scope | tac2type5 ltac2_type | tac2type2 ltac2_type2 | tac2type1 ltac2_type1 | tac2type0 ltac2_type0 | typ_param ltac2_typevar | tac2expr6 ltac2_expr | tac2expr5 ltac2_expr5 | tac2expr3 ltac2_expr3 | tac2expr2 ltac2_expr2 | tac2expr1 ltac2_expr1 | tac2expr0 ltac2_expr0 | gmatch_list goal_match_list ] simple_tactic: [ (* due to renaming of tactic_arg; Use LIST1 for function application *) | qualid LIST1 tactic_arg ] (* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *) clause_dft_concl: [ | OPTINREF ] SPLICE: [ | gallina | gallina_ext | syntax | vernac_control | vernac_toplevel | command_entry | ltac_builtins | ltac_constructs | ltac2_constructs | ltac_defined_tactics | tactic_notation_tactics ] (* todo: ssrreflect*.rst ref to fix_body is incorrect *) REACHABLE: [ | command | simple_tactic ] NOTINRSTS: [ | simple_tactic | REACHABLE | NOTINRSTS | l1_tactic | l2_tactic | l3_tactic | binder_tactic | value_tactic | ltac2_entry (* ltac2 syntactic classes *) | q_intropatterns | q_intropattern | q_ident | q_destruction_arg | q_with_bindings | q_bindings | q_strategy_flag | q_reference | q_clause | q_occurrences | q_induction_clause | q_conversion | q_rewriting | q_dispatch | q_hintdb | q_move_location | q_pose | q_assert | q_constr_matching | q_goal_matching (* todo: figure these out (*Warning: editedGrammar: Undefined symbol 'ltac1_expr' *) | dangling_pattern_extension_rule | vernac_aux | subprf | tactic_mode | tac2expr_in_env (* no refs *) | tac2mode (* no refs *) | ltac_use_default (* from tac2mode *) | tacticals *) ] REACHABLE: [ | NOTINRSTS ]