(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* " LIST1 global OPT natural | WITH "Resolve" [ "->" | "<-" ] LIST1 global OPT natural | DELETE "Resolve" "<-" LIST1 global OPT natural | REPLACE "Variables" "Transparent" | WITH [ "Constants" | "Variables" ] [ "Transparent" | "Opaque" ] | DELETE "Variables" "Opaque" | DELETE "Constants" "Transparent" | DELETE "Constants" "Opaque" | REPLACE "Transparent" LIST1 global | WITH [ "Transparent" | "Opaque" ] LIST1 global | DELETE "Opaque" LIST1 global | REPLACE "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic | WITH "Extern" natural OPT constr_pattern "=>" tactic | INSERTALL "Hint" | APPENDALL opt_hintbases ] (* 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 ] EXTRAARGS_natural: [ | DELETENT ] EXTRAARGS_lconstr: [ | DELETENT ] EXTRAARGS_strategy_level: [ | DELETENT ] binders: [ | DELETE Pcoq.Constr.binders ] G_TACTIC_in_clause: [ | in_clause | MOVEALLBUT in_clause | in_clause ] SPLICE: [ | G_TACTIC_in_clause ] RENAME: [ | G_LTAC2_delta_flag ltac2_delta_reductions | G_LTAC2_strategy_flag ltac2_reductions | 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_for_each_goal ltac2_for_each_goal | 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 | G_SSRMATCHING_cpattern ssr_one_term_pattern ] (* 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.cpattern cpattern | G_vernac.query_command query_command | G_vernac.section_subset_expr section_var_expr | Prim.ident ident | Prim.reference reference | Prim.string string | Prim.integer integer | Prim.qualid qualid | Prim.natural natural | Pvernac.Vernac_.main_entry vernac_control | Tactic.tactic tactic | Pltac.ltac_expr ltac_expr5 (* SSR *) | Pcoq.Constr.constr term | Prim.identref ident (* | G_vernac.def_body def_body | Prim.by_notation by_notation | Prim.natural natural *) | Vernac.fix_definition fix_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 | test_variance_ident (* SSR *) | ssr_null_entry | ssrtermkind (* todo: rename as "test..." *) | ssrdoarg (* todo: this and the next one should be removed from the grammar? *) | ssrseqdir | ssrindex | ssrintrosarg | ssrtclarg | term_annotation (* todo: what is this? *) | test_idcomma | test_ident_no_do | test_nohidden | test_not_ssrslashnum | test_ssr_rw_syntax | test_ssreqid | test_ssrfwdid | test_ssrseqvar | test_ssrslashnum00 | test_ssrslashnum01 | test_ssrslashnum10 | test_ssrslashnum11 (* unused *) | constr_comma_sequence' | auto_using' | constr_may_eval ] (* additional nts to be spliced *) tactic_then_last: [ | REPLACE "|" LIST0 ( OPT ltac_expr5 ) SEP "|" | WITH LIST0 ( "|" ( OPT ltac_expr5 ) ) ] goal_tactics: [ | LIST0 ( OPT ltac_expr5 ) SEP "|" ] for_each_goal: [ | DELETENT ] for_each_goal: [ | goal_tactics | OPT ( goal_tactics "|" ) OPT ltac_expr5 ".." OPT ( "|" goal_tactics ) ] ltac2_tactic_then_last: [ | REPLACE "|" LIST0 ( OPT ltac2_expr6 ) SEP "|" (* Ltac2 plugin *) | WITH LIST0 ( "|" OPT ltac2_expr6 ) TAG Ltac2 ] ltac2_goal_tactics: [ | LIST0 ( OPT ltac2_expr6 ) SEP "|" TAG Ltac2 ] ltac2_for_each_goal: [ | DELETENT ] ltac2_for_each_goal: [ | ltac2_goal_tactics TAG Ltac2 | OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr6 ".." OPT ( "|" ltac2_goal_tactics ) TAG Ltac2 ] 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 ] case_item: [ | REPLACE term100 OPT [ "as" name ] OPT [ "in" pattern200 ] | WITH term100 OPT ("as" name) OPT [ "in" pattern200 ] ] binder_constr: [ | MOVETO term_forall_or_fun "forall" open_binders "," term200 | MOVETO term_forall_or_fun "fun" open_binders "=>" term200 | MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200 (*| MOVETO term_let "let" ":" ssr_mpat ":=" lconstr "in" lconstr TAG SSR *) | DELETE "let" ":" ssr_mpat ":=" lconstr "in" lconstr TAG SSR (* todo: restore for ssr *) | REPLACE "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) | WITH "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr TAG SSR | DELETE "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* SSR plugin *) | DELETE "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr TAG SSR (* todo: restore for SSR *) (*| MOVETO term_let "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr TAG SSR*) | MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200 | REPLACE "if" term200 "is" ssr_dthen ssr_else | WITH "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else TAG SSR | DELETE "if" term200 "isn't" ssr_dthen ssr_else | DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else TAG SSR (* todo: restore as "MOVETO term_if" for SSR *) | MOVETO term_fix "let" "fix" fix_decl "in" term200 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 | MOVETO term_let "let" "'" pattern200 ":=" term200 "in" term200 | MOVETO term_let "let" "'" pattern200 ":=" term200 case_type "in" term200 | MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 | MOVETO term_fix "fix" fix_decls | MOVETO term_cofix "cofix" cofix_decls ] term_let: [ | REPLACE "let" name binders let_type_cstr ":=" term200 "in" term200 | WITH "let" name let_type_cstr ":=" term200 "in" term200 | "let" name LIST1 binder let_type_cstr ":=" term200 "in" term200 (* Don't need to document that "( )" is equivalent to "()" *) | REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 | WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200 | MOVETO destructuring_let "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200 | REPLACE "let" "'" pattern200 ":=" term200 "in" term200 | WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200 | DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200 | MOVETO destructuring_let "let" "'" pattern200 ":=" term200 OPT case_type "in" term200 | MOVETO destructuring_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 ] atomic_constr: [ | MOVETO qualid_annotated global univ_annot | MOVETO primitive_notations NUMBER | MOVETO primitive_notations string | MOVETO term_evar "_" | REPLACE "?" "[" identref "]" | WITH "?[" identref "]" | MOVETO term_evar "?[" identref "]" | REPLACE "?" "[" pattern_ident "]" | WITH "?[" pattern_ident "]" | MOVETO term_evar "?[" pattern_ident "]" | MOVETO term_evar pattern_ident evar_instance ] ltac_expr0: [ | REPLACE "[" ">" for_each_goal "]" | WITH "[>" for_each_goal "]" | DELETE ssrparentacarg ] (* lexer token *) IDENT: [ | ident ] scope_key: [ | IDENT ] scope_name: [ | IDENT ] scope: [ | scope_name | scope_key ] scope_delimiter: [ | REPLACE "%" IDENT | WITH "%" scope_key ] type: [ | term200 ] term100: [ | REPLACE term99 "<:" term200 | WITH term99 "<:" type | MOVETO term_cast term99 "<:" type | REPLACE term99 "<<:" term200 | WITH term99 "<<:" type | MOVETO term_cast term99 "<<:" type | REPLACE term99 ":" term200 | WITH term99 ":" type | MOVETO term_cast term99 ":" type ] constr: [ | REPLACE "@" global univ_annot | WITH "@" qualid_annotated | MOVETO term_explicit "@" qualid_annotated ] term10: [ (* Separate this LIST0 in the nonempty and the empty case *) (* The empty case is covered by constr *) | REPLACE "@" global univ_annot LIST0 term9 | WITH "@" qualid_annotated LIST1 term9 | REPLACE term9 | WITH constr | MOVETO term_application term9 LIST1 arg | MOVETO term_application "@" qualid_annotated LIST1 term9 (* fixme: add in as a prodn somewhere *) | MOVETO dangling_pattern_extension_rule "@" pattern_ident LIST1 identref | DELETE dangling_pattern_extension_rule ] term9: [ (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *) | DELETE ".." term0 ".." ] term1: [ | REPLACE term0 ".(" global LIST0 arg ")" | WITH term0 ".(" global LIST0 arg ")" (* huh? *) | REPLACE term0 "%" IDENT | WITH term0 "%" scope_key | MOVETO term_scope term0 "%" scope_key | MOVETO term_projection term0 ".(" global LIST0 arg ")" | MOVETO term_projection term0 ".(" "@" global LIST0 ( term9 ) ")" ] term0: [ (* @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 SEP ";" OPT ";" bar_cbrace | MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace | MOVETO term_generalizing "`{" term200 "}" | MOVETO term_generalizing "`(" term200 ")" | MOVETO term_ltac "ltac" ":" "(" ltac_expr5 ")" | REPLACE "[" "|" array_elems "|" lconstr type_cstr "|" "]" univ_annot | WITH "[|" array_elems "|" lconstr type_cstr "|]" univ_annot ] 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_body | REPLACE cofix_body "with" LIST1 cofix_body SEP "with" "for" identref | WITH cofix_body OPT ( LIST1 ( "with" cofix_body ) "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 ":" type (* @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 "," "]" | DELETE [ "of" | "&" ] term99 (* todo: remove for SSR *) ] name_colon: [ | name ":" ] typeclass_constraint: [ | EDIT ADD_OPT "!" term200 | REPLACE "{" name "}" ":" [ "!" | ] term200 | WITH "{" name "}" ":" OPT "!" term200 | REPLACE name ":" [ "!" | ] term200 | WITH name ":" OPT "!" term200 ] (* ?? 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 ] (* No constructor syntax, OPT [ "|" binders ] is not supported for Record *) record_definition: [ | opt_coercion ident_decl binders OPT [ ":" sort ] OPT ( ":=" OPT [ identref ] "{" record_fields "}" ) ] (* No mutual recursion, no inductive classes, type must be a sort *) (* constructor is optional but "Class record_definition" covers that case *) singleton_class_definition: [ | opt_coercion ident_decl binders OPT [ ":" sort ] ":=" constructor ] (* 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" record_definition | "Class" singleton_class_definition | REPLACE "Fixpoint" LIST1 fix_definition SEP "with" | WITH "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) | REPLACE "Let" "Fixpoint" LIST1 fix_definition SEP "with" | WITH "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) | REPLACE "CoFixpoint" LIST1 cofix_definition SEP "with" | WITH "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) | REPLACE "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" | WITH "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) | REPLACE "Scheme" LIST1 scheme SEP "with" | WITH "Scheme" scheme LIST0 ( "with" scheme ) ] finite_token: [ | DELETENT ] record_fields: [ | REPLACE record_field ";" record_fields | WITH LIST0 record_field SEP ";" OPT ";" | DELETE record_field | DELETE (* empty *) ] assumptions_token: [ | DELETENT ] inline: [ | REPLACE "Inline" "(" natural ")" | WITH "Inline" OPT ( "(" natural ")" ) | DELETE "Inline" ] univ_decl: [ | REPLACE "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] | WITH "@{" LIST0 identref OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] cumul_univ_decl: [ | REPLACE "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] | WITH "@{" LIST0 variance_identref OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] of_type: [ | DELETENT ] of_type: [ | [ ":" | ":>" ] type ] 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 ] delta_flag: [ | REPLACE "-" "[" LIST1 smart_global "]" | WITH OPT "-" "[" LIST1 smart_global "]" | DELETE "[" LIST1 smart_global "]" | OPTINREF ] ltac2_delta_reductions: [ | EDIT ADD_OPT "-" "[" refglobals "]" (* Ltac2 plugin *) ] ltac2_branches: [ | EDIT ADD_OPT "|" LIST1 branch SEP "|" (* Ltac2 plugin *) ] strategy_flag: [ | REPLACE OPT delta_flag | WITH delta_flag (*| REPLACE LIST1 red_flags | WITH LIST1 red_flag*) | (* empty *) ] filtered_import: [ | REPLACE global "(" LIST1 one_import_filter_name SEP "," ")" | WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ] | DELETE global ] is_module_expr: [ | REPLACE ":=" module_expr_inl LIST0 ext_module_expr | WITH ":=" LIST1 module_expr_inl SEP "<+" ] is_module_type: [ | REPLACE ":=" module_type_inl LIST0 ext_module_type | WITH ":=" LIST1 module_type_inl SEP "<+" ] gallina_ext: [ | REPLACE "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ] | WITH "Arguments" smart_global LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_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 (* semantically restricted per https://github.com/coq/coq/pull/12936#discussion_r492705820 *) | REPLACE "Coercion" global OPT univ_decl def_body | WITH "Coercion" ident OPT univ_decl def_body | 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" setting_name option_setting | WITH "Set" setting_name option_setting | REPLACE "Export" "Unset" setting_name | WITH "Unset" setting_name | REPLACE "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] | WITH "Instance" instance_name ":" type hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ] | REPLACE "From" global "Require" export_token LIST1 global | WITH "From" dirpath "Require" export_token LIST1 global ] (* lexer stuff *) LEFTQMARK: [ | "?" ] digit: [ | "0" ".." "9" ] decnat: [ | digit LIST0 [ digit | "_" ] ] hexdigit: [ | [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ] ] hexnat: [ | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ] ] bignat: [ | REPLACE NUMBER | WITH [ decnat | hexnat ] ] integer: [ | REPLACE bigint | WITH OPT "-" natural ] number: [ | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat ) | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] bigint: [ | DELETE bignat | REPLACE test_minus_nat "-" bignat | WITH OPT "-" bignat ] first_letter: [ | [ "a" ".." "z" | "A" ".." "Z" | "_" | unicode_letter ] ] subsequent_letter: [ | [ first_letter | digit | "'" | unicode_id_part ] ] ident: [ | DELETE IDENT | DELETE IDENT (* 2nd copy from SSR *) | first_letter LIST0 subsequent_letter ] NUMBER: [ | number ] (* 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 ] ltac_expr5: [ (* make these look consistent with use of binder_tactic in other ltac_expr* *) | DELETE binder_tactic | DELETE ltac_expr4 | [ ltac_expr4 | binder_tactic ] ] ltac_constructs: [ (* repeated in main ltac grammar - need to create a COPY edit *) | ltac_expr3 ";" [ ltac_expr3 | binder_tactic ] | ltac_expr3 ";" "[" for_each_goal "]" | ltac_expr1 "+" [ ltac_expr2 | binder_tactic ] | ltac_expr1 "||" [ ltac_expr2 | binder_tactic ] (* | qualid LIST0 tactic_value add later due renaming tactic_value *) | "[>" for_each_goal "]" | toplevel_selector ltac_expr5 ] ltac_expr4: [ | REPLACE ltac_expr3 ";" for_each_goal "]" | WITH ltac_expr3 ";" "[" for_each_goal "]" | REPLACE ltac_expr3 ";" binder_tactic | WITH ltac_expr3 ";" [ ltac_expr3 | binder_tactic ] | DELETE ltac_expr3 ";" ltac_expr3 | MOVETO simple_tactic ltac_expr5 ";" "first" ssr_first_else TAG SSR | MOVETO simple_tactic ltac_expr5 ";" "first" ssrseqarg TAG SSR | MOVETO simple_tactic ltac_expr5 ";" "last" ssrseqarg TAG SSR | DELETE simple_tactic ] l3_tactic: [ ] ltac_expr3: [ | DELETE "abstract" ltac_expr2 | REPLACE "abstract" ltac_expr2 "using" ident | WITH "abstract" ltac_expr2 OPT ( "using" ident ) | l3_tactic (* | EDIT "do" ADD_OPT nat_or_var ssrmmod ssrdotac ssrclauses TAG SSR *) | DELETE "do" ssrmmod ssrdotac ssrclauses (* SSR plugin *) | DELETE "do" ssrortacarg ssrclauses (* SSR plugin *) | DELETE "do" nat_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) | MOVEALLBUT ltac_builtins | l3_tactic | ltac_expr2 ] l2_tactic: [ ] ltac_expr2: [ | REPLACE ltac_expr1 "+" binder_tactic | WITH ltac_expr1 "+" [ ltac_expr2 | binder_tactic ] | DELETE ltac_expr1 "+" ltac_expr2 | REPLACE ltac_expr1 "||" binder_tactic | WITH ltac_expr1 "||" [ ltac_expr2 | binder_tactic ] | DELETE ltac_expr1 "||" ltac_expr2 | MOVETO ltac_builtins "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2 | l2_tactic | DELETE ltac_builtins ] l1_tactic: [ ] ltac_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 ltac_expr5 "with" match_list "end" | REPLACE failkw [ nat_or_var | ] LIST0 message_token | WITH failkw OPT nat_or_var LIST0 message_token | REPLACE reference LIST0 tactic_arg | WITH reference LIST1 tactic_arg | l1_tactic | DELETE simple_tactic | MOVEALLBUT ltac_builtins | l1_tactic | tactic_value | reference LIST1 tactic_arg | ltac_expr0 ] (* split match_context_rule *) goal_pattern: [ | LIST0 match_hyp SEP "," "|-" match_pattern | "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" | "_" ] match_context_rule: [ | DELETE LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr5 | DELETE "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr5 | DELETE "_" "=>" ltac_expr5 | goal_pattern "=>" ltac_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 "_" "=>" ltac_expr5 ] selector: [ | 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_occurrences: [ (* placeholder (yuck) *) ] simple_tactic: [ | REPLACE "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases | WITH "eauto" OPT nat_or_var auto_using hintbases | REPLACE "debug" "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases | WITH "debug" "eauto" OPT nat_or_var auto_using hintbases | REPLACE "info_eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases | WITH "info_eauto" OPT nat_or_var auto_using hintbases | 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 ) | REPLACE "autounfold" hintbases clause_dft_concl | WITH "autounfold" hintbases OPT simple_occurrences | REPLACE "red" clause_dft_concl | WITH "red" simple_occurrences | REPLACE "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl | WITH "simpl" OPT delta_flag OPT ref_or_pattern_occ simple_occurrences | REPLACE "hnf" clause_dft_concl | WITH "hnf" simple_occurrences | REPLACE "cbv" strategy_flag clause_dft_concl | WITH "cbv" strategy_flag simple_occurrences | PRINT | REPLACE "compute" OPT delta_flag clause_dft_concl | WITH "compute" OPT delta_flag simple_occurrences | REPLACE "lazy" strategy_flag clause_dft_concl | WITH "lazy" strategy_flag simple_occurrences | REPLACE "cbn" strategy_flag clause_dft_concl | WITH "cbn" strategy_flag simple_occurrences | REPLACE "fold" LIST1 constr clause_dft_concl | WITH "fold" LIST1 constr simple_occurrences | DELETE "cofix" ident | REPLACE "cofix" ident "with" LIST1 cofixdecl | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl ) | DELETE "constructor" | DELETE "constructor" nat_or_var | REPLACE "constructor" nat_or_var "with" bindings | WITH "constructor" OPT nat_or_var OPT ( "with" bindings ) | DELETE "econstructor" | DELETE "econstructor" nat_or_var | REPLACE "econstructor" nat_or_var "with" bindings | WITH "econstructor" OPT ( nat_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 "intros" | REPLACE "intros" ne_intropatterns | WITH "intros" intropatterns | DELETE "eintros" | REPLACE "eintros" ne_intropatterns | WITH "eintros" intropatterns | 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" nat_or_var "in" constr | WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" nat_or_var ) "in" constr | DELETE "hresolve_core" "(" ident ":=" constr ")" "in" constr | EDIT "psatz_R" ADD_OPT nat_or_var tactic | EDIT "psatz_Q" ADD_OPT nat_or_var tactic | EDIT "psatz_Z" ADD_OPT nat_or_var tactic | REPLACE "subst" LIST1 hyp | WITH "subst" LIST0 hyp | DELETE "subst" | DELETE "congruence" | DELETE "congruence" natural | DELETE "congruence" "with" LIST1 constr | REPLACE "congruence" natural "with" LIST1 constr | WITH "congruence" OPT natural OPT ( "with" LIST1 constr ) | DELETE "show" "ltac" "profile" | REPLACE "show" "ltac" "profile" "cutoff" integer | WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ] | DELETE "show" "ltac" "profile" string (* perversely, the mlg uses "tactic3" instead of "ltac_expr3" *) | DELETE "transparent_abstract" tactic3 | REPLACE "transparent_abstract" tactic3 "using" ident | WITH "transparent_abstract" ltac_expr3 OPT ( "using" ident ) | "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 preident ) | DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident | DELETE "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident | DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var | DELETE "typeclasses" "eauto" OPT nat_or_var (* in Tactic Notation: *) | "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 ) | REPLACE "apply" ssrapplyarg (* SSR plugin *) | WITH "apply" OPT ssrapplyarg TAG SSR | DELETE "apply" | REPLACE "elim" ssrarg ssrclauses (* SSR plugin *) | WITH "elim" OPT ( ssrarg ssrclauses ) TAG SSR | DELETE "elim" (* SSR plugin *) | REPLACE "case" ssrcasearg ssrclauses (* SSR plugin *) | WITH "case" OPT ( ssrcasearg ssrclauses ) TAG SSR | DELETE "case" (* SSR plugin *) | REPLACE "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* SSR plugin *) | WITH "under" ssrrwarg OPT ssrintros_ne OPT ( "do" ssrhint3arg ) TAG SSR | DELETE "under" ssrrwarg (* SSR plugin *) | DELETE "under" ssrrwarg ssrintros_ne (* SSR plugin *) | DELETE "under" ssrrwarg "do" ssrhint3arg (* SSR plugin *) | REPLACE "move" ssrmovearg ssrrpat (* SSR plugin *) | WITH "move" OPT ( OPT ssrmovearg ssrrpat ) TAG SSR | DELETE "move" ssrrpat (* SSR plugin *) | DELETE "move" (* SSR plugin *) | REPLACE "suff" "have" ssrhpats_nobs ssrhavefwd (* SSR plugin *) | WITH [ "suff" | "suffices" ] OPT ( "have" ssrhpats_nobs ) ssrhavefwd TAG SSR | DELETE "suffices" "have" ssrhpats_nobs ssrhavefwd (* SSR plugin *) | REPLACE "suff" ssrsufffwd (* SSR plugin *) | WITH [ "suff" | "suffices" ] ssrsufffwd TAG SSR | DELETE "suffices" ssrsufffwd (* SSR plugin *) | REPLACE "have" "suff" ssrhpats_nobs ssrhavefwd (* SSR plugin *) | WITH "have" [ "suff" | "suffices" ] ssrhpats_nobs ssrhavefwd TAG SSR | DELETE "have" "suffices" ssrhpats_nobs ssrhavefwd (* SSR plugin *) | REPLACE "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) | WITH [ "gen" | "generally" ] "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint TAG SSR | DELETE "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) | REPLACE "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) | WITH [ "wlog" | "without loss" ] OPT [ "suff" | "suffices" ] ssrhpats_nobs ssrwlogfwd ssrhint TAG SSR | DELETE "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) | DELETE "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) | DELETE "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) | DELETE "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) | DELETE "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) ] (* 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 *) | REPLACE "Hint" | WITH "Hint" OPT [ "*" | smart_global ] | DELETE "Hint" smart_global | DELETE "Hint" "*" | INSERTALL "Print" ] add_zify: [ | [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ] TAG Micromega | [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]TAG Micromega ] show_zify: [ | [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ] TAG Micromega ] scheme_kind: [ | DELETE "Induction" "for" smart_global "Sort" sort_family | DELETE "Minimality" "for" smart_global "Sort" sort_family | DELETE "Elimination" "for" smart_global "Sort" sort_family | DELETE "Case" "for" smart_global "Sort" sort_family | [ "Induction" | "Minimality" | "Elimination" | "Case" ] "for" smart_global "Sort" sort_family ] command: [ | REPLACE "Print" printable | WITH printable | REPLACE "Hint" hint opt_hintbases | WITH hint | "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_fix_definition SEP "with" (* funind plugin *) | WITH "Function" function_fix_definition LIST0 ( "with" function_fix_definition ) (* 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" setting_name | REPLACE "Set" setting_name option_setting | WITH OPT "Export" "Set" setting_name (* set flag *) | REPLACE "Test" setting_name "for" LIST1 table_value | WITH "Test" setting_name OPT ( "for" LIST1 table_value ) | DELETE "Test" setting_name (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Add" IDENT IDENT LIST1 table_value | WITH "Add" setting_name 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" natural "of" ident ":" lglob withtac | WITH "Obligation" natural OPT ( "of" ident ) OPT ( ":" type withtac ) | DELETE "Obligation" natural "of" ident withtac | DELETE "Obligation" natural ":" lglob withtac | DELETE "Obligation" natural withtac | REPLACE "Obligations" "of" ident | WITH "Obligations" OPT ( "of" ident ) | DELETE "Obligations" | REPLACE "Preterm" "of" ident | WITH "Preterm" OPT ( "of" ident ) | DELETE "Preterm" | REPLACE "Proof" "using" section_var_expr "with" Pltac.tactic | WITH "Proof" "using" section_subset_expr OPT [ "with" ltac_expr5 ] | DELETE "Proof" "using" section_var_expr (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Remove" IDENT IDENT LIST1 table_value | WITH "Remove" setting_name 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" integer | WITH "Show" "Ltac" "Profile" OPT [ "CutOff" integer | 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" | DELETE "Solve" "Obligations" "of" ident "with" tactic | DELETE "Solve" "Obligations" "of" ident | DELETE "Solve" "Obligations" "with" tactic | DELETE "Solve" "Obligations" | "Solve" "Obligations" OPT ( "of" ident ) OPT ( "with" tactic ) | REPLACE "Solve" "Obligation" natural "of" ident "with" tactic | WITH "Solve" "Obligation" natural OPT ( "of" ident ) "with" tactic | DELETE "Solve" "Obligation" natural "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 "Number" "Notation" reference reference reference OPT number_options ":" ident | WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name | REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier | WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier | REPLACE "String" "Notation" reference reference reference OPT string_option ":" ident | WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name | DELETE "Ltac2" ltac2_entry (* was split up *) | DELETE "Add" "Zify" "InjTyp" constr (* micromega plugin *) | DELETE "Add" "Zify" "BinOp" constr (* micromega plugin *) | DELETE "Add" "Zify" "UnOp" constr (* micromega plugin *) | DELETE "Add" "Zify" "CstOp" constr (* micromega plugin *) | DELETE "Add" "Zify" "BinRel" constr (* micromega plugin *) | DELETE "Add" "Zify" "PropOp" constr (* micromega plugin *) | DELETE "Add" "Zify" "PropBinOp" constr (* micromega plugin *) | DELETE "Add" "Zify" "PropUOp" constr (* micromega plugin *) | DELETE "Add" "Zify" "BinOpSpec" constr (* micromega plugin *) | DELETE "Add" "Zify" "UnOpSpec" constr (* micromega plugin *) | DELETE "Add" "Zify" "Saturate" constr (* micromega plugin *) | "Add" "Zify" add_zify constr TAG Micromega | DELETE "Show" "Zify" "InjTyp" (* micromega plugin *) | DELETE "Show" "Zify" "BinOp" (* micromega plugin *) | DELETE "Show" "Zify" "UnOp" (* micromega plugin *) | DELETE "Show" "Zify" "CstOp" (* micromega plugin *) | DELETE "Show" "Zify" "BinRel" (* micromega plugin *) | DELETE "Show" "Zify" "UnOpSpec" (* micromega plugin *) | DELETE "Show" "Zify" "BinOpSpec" (* micromega plugin *) (* keep this one | "Show" "Zify" "Spec" (* micromega plugin *)*) | "Show" "Zify" show_zify TAG Micromega | REPLACE "Goal" lconstr | WITH "Goal" type ] 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 ] explicit_subentry: [ | 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 *) ] binder_tactic: [ | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5 | MOVEALLBUT ltac_builtins ] field_body: [ | REPLACE binders of_type lconstr | WITH binders of_type | REPLACE binders of_type lconstr ":=" lconstr | WITH binders of_type ":=" lconstr ] assumpt: [ | REPLACE LIST1 ident_decl of_type lconstr | WITH LIST1 ident_decl of_type ] constructor_type: [ | REPLACE binders [ of_type lconstr | ] | WITH binders OPT of_type ] (* 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 *) fix_definition: [ | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations | WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] cofix_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 ] inductive_definition: [ | REPLACE opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations | WITH opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations ] (* note that constructor -> identref constructor_type *) constructors_or_record: [ | 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 field_body | WITH name OPT field_body | DELETE name ] 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 "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 ] 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 ] of_module_type: [ | (* empty *) ] 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 ] ltac2_expr0: [ | 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 ] constr_body: [ | DELETE ":=" lconstr | REPLACE ":" lconstr ":=" lconstr | WITH OPT ( ":" type ) ":=" lconstr ] scheme: [ | DELETE scheme_kind | REPLACE identref ":=" scheme_kind | WITH OPT ( identref ":=" ) scheme_kind ] simple_reserv: [ | REPLACE LIST1 identref ":" lconstr | WITH LIST1 identref ":" type ] in_clause: [ | DELETE in_clause' | REPLACE LIST1 hypident_occ SEP "," "|-" concl_occ | WITH LIST1 hypident_occ SEP "," OPT ( "|-" concl_occ ) | DELETE LIST1 hypident_occ SEP "," | REPLACE "*" occs | WITH concl_occ (* todo: perhaps concl_occ should be "*" | "at" occs_nums *) ] 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 *) ] decl_notations: [ | REPLACE "where" LIST1 decl_notation SEP decl_sep | WITH "where" decl_notation LIST0 (decl_sep decl_notation ) ] 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 ] ] 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 ":=" ltac_expr5 | REPLACE "_" ":=" ltac_expr5 | WITH name ":=" ltac_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 | REPLACE OPT toplevel_selector "{" (* semantically restricted *) | WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{" | MOVETO simple_tactic OPT ( [ natural | "[" ident "]" ] ":" ) "{" | DELETE simple_tactic ] tactic_mode: [ | DELETENT ] ltac2_scope: [ | REPLACE syn_node (* Ltac2 plugin *) | WITH name TAG Ltac2 | REPLACE syn_node "(" LIST1 ltac2_scope SEP "," ")" (* Ltac2 plugin *) | WITH name "(" LIST1 ltac2_scope SEP "," ")" TAG Ltac2 ] syn_node: [ | DELETENT ] RENAME: [ | toplevel_selector toplevel_selector_temp ] toplevel_selector: [ | selector | "all" | "!" (* par is accepted even though it's not in the .mlg *) | "par" ] toplevel_selector_temp: [ | DELETE selector ":" | 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 ( natural ":" ) query_command "." | OPT attributes OPT ( toplevel_selector ":" ) ltac_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" | "now_show" constr | "nra" | "over" TAG SSR | "split_Rabs" | "split_Rmult" | "tauto" | "time_constr" ltac_expr5 | "zify" ] (* todo: need careful review; assume that "[" ... "]" are literals *) tactic_notation_tactics: [ | "assert_fails" ltac_expr3 | "assert_succeeds" ltac_expr3 | "dintuition" OPT ltac_expr5 | "dtauto" | "field" OPT ( "[" LIST1 constr "]" ) | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident ) | "intuition" OPT ltac_expr5 (* todo: Not too keen on things like "with_power_flags" in tauto.ml, not easy to follow *) | "now" ltac_expr5 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr ) | "psatz" constr OPT nat_or_var | "ring" OPT ( "[" LIST1 constr "]" ) | "ring_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) (* todo: ident was "hyp", worth keeping? *) ] (* defined in OCaml outside of mlgs *) tactic_value: [ | "uconstr" ":" "(" term200 ")" | MOVEALLBUT simple_tactic ] nonterminal: [ ] value_tactic: [ ] 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 ltac2_expr6 "with" ltac2_match_list "end" | ltac2_match_key OPT "reverse" "goal" "with" goal_match_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 ltac_expr5 | WITH global LIST0 input_fun ltac_def_kind ltac_expr5 | DELETE global ltac_def_kind ltac_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 ] rec_flag: [ | OPTINREF ] ltac2_orient: [ | DELETENT ] ltac2_orient: [ | orient ] SPLICE: [ | ltac2_orient ] ltac2_expr0: [ (* | DELETE "(" ")" (* covered by "()" prodn *) | REPLACE "{" [ | LIST1 tac2rec_fieldexpr OPT ";" ] "}" | WITH "{" OPT ( LIST1 tac2rec_fieldexpr OPT ";" ) "}" *) ] (* todo: should | tac2pat1 "," LIST0 tac2pat1 SEP "," use LIST1? *) SPLICE: [ | ltac2_expr4 ] ltac2_expr3: [ | REPLACE ltac2_expr2 "," LIST1 ltac2_expr2 SEP "," (* Ltac2 plugin *) | WITH LIST1 ltac2_expr2 SEP "," TAG Ltac2 | DELETE ltac2_expr2 (* Ltac2 plugin *) ] tac2rec_fieldexprs: [ | DELETE tac2rec_fieldexpr ";" tac2rec_fieldexprs | DELETE tac2rec_fieldexpr ";" | DELETE tac2rec_fieldexpr | LIST1 tac2rec_fieldexpr OPT ";" ] tac2rec_fields: [ | DELETE tac2rec_field ";" tac2rec_fields | DELETE tac2rec_field ";" | DELETE tac2rec_field | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 ] int_or_var: [ | REPLACE integer | WITH [ integer | identref ] | DELETE identref ] nat_or_var: [ | REPLACE natural | WITH [ natural | identref ] | DELETE identref ] 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 ] 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 ] ":=" ltac2_expr6 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 | rec_flag | locident | tac2alg_constructors | ltac2_binder | branch | anti ] ltac2_expr5: [ | REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *) | WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2 | MOVETO simple_tactic "match" ltac2_expr5 "with" ltac2_branches "end" (* Ltac2 plugin *) | MOVETO simple_tactic "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *) | DELETE simple_tactic ] goal_match_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 "pat" ":" "(" 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 ltac2_as_or_and_ipat ltac2_eqn_ipat OPT clause (* Ltac2 plugin *) | WITH ltac2_destruction_arg ltac2_as_or_and_ipat ltac2_eqn_ipat OPT ltac2_clause TAG Ltac2 ] starredidentref: [ | EDIT identref ADD_OPT "*" | EDIT "Type" ADD_OPT "*" | "All" ] ssexpr0: [ | DELETE "(" LIST0 starredidentref ")" | DELETE "(" LIST0 starredidentref ")" "*" | DELETE "(" ssexpr35 ")" | DELETE "(" ssexpr35 ")" "*" | "(" section_subset_expr ")" OPT "*" ] ssexpr35: [ | EDIT ADD_OPT "-" ssexpr50 ] simple_binding: [ | REPLACE "(" ident ":=" lconstr ")" | WITH "(" [ ident | natural ] ":=" lconstr ")" | DELETE "(" natural ":=" lconstr ")" ] subprf: [ | MOVEALLBUT simple_tactic | "{" (* should be removed. See https://github.com/coq/coq/issues/12004 *) ] ltac2_expr: [ | DELETE _ltac2_expr ] ssrfwdview: [ | REPLACE "/" ast_closure_term ssrfwdview (* SSR plugin *) | WITH LIST1 ( "/" ast_closure_term ) TAG SSR | DELETE "/" ast_closure_term (* SSR plugin *) ] ssrfwd: [ | REPLACE ":" ast_closure_lterm ":=" ast_closure_lterm (* SSR plugin *) | WITH OPT ( ":" ast_closure_lterm ) ":=" ast_closure_lterm TAG SSR | DELETE ":=" ast_closure_lterm (* SSR plugin *) ] ssrsetfwd: [ | REPLACE ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* SSR plugin *) | WITH OPT ( ":" ast_closure_lterm ) ":=" [ "{" ssrocc "}" cpattern | lcpattern ] TAG SSR | DELETE ":" ast_closure_lterm ":=" lcpattern (* SSR plugin *) | DELETE ":=" "{" ssrocc "}" cpattern (* SSR plugin *) | DELETE ":=" lcpattern (* SSR plugin *) ] (* per @gares *) ssrdgens: [ | REPLACE ":" ssrgen ssrdgens_tl (* SSR plugin *) | WITH ":" ssrgen OPT ( "/" ssrgen ) TAG SSR ] ssrdgens_tl: [ | DELETENT ] ssrgen: [ | REPLACE ssrdocc cpattern (* SSR plugin *) | WITH cpattern LIST0 [ LIST1 ident | cpattern ] TAG SSR | DELETE cpattern (* SSR plugin *) ] OPTINREF: [ ] ssrortacs: [ | EDIT ssrtacarg "|" ADD_OPT ssrortacs (* ssr plugin *) | EDIT "|" ADD_OPT ssrortacs (* ssr plugin *) | EDIT ADD_OPT ssrtacarg "|" OPT ssrortacs ] ssrocc: [ | REPLACE natural LIST0 natural (* SSR plugin *) | WITH [ natural | "+" | "-" ] LIST0 natural TAG SSR | DELETE "-" LIST0 natural (* SSR plugin *) | DELETE "+" LIST0 natural (* SSR plugin *) ] ssripat: [ | DELETE ssrdocc "->" (* SSR plugin *) | DELETE ssrdocc "<-" (* SSR plugin *) | REPLACE ssrdocc (* SSR plugin *) | WITH ssrdocc OPT [ "->" | "<-" ] TAG SSR | DELETE "->" (* SSR plugin *) | DELETE "<-" (* SSR plugin *) | DELETE "-/" "=" (* SSR plugin *) | DELETE "-/" "/" (* SSR plugin *) | DELETE "-/" integer "/" (* SSR plugin *) | DELETE "-/" integer "/=" (* SSR plugin *) | REPLACE "-/" integer "/" integer "=" (* SSR plugin *) | WITH "-/" integer [ "/=" | "/" | "/" integer "=" ] TAG SSR | DELETE "-/" "/=" (* SSR plugin *) | DELETE "-//" "=" (* SSR plugin *) | DELETE "[" ":" LIST0 ident "]" (* SSR plugin *) ] ssrsimpl_ne: [ | DELETE "/" natural "/" "=" (* SSR plugin *) (* parsed but not supported per @gares *) | DELETE "/" natural "/" (* SSR plugin *) | DELETE "/" natural "=" (* SSR plugin *) | DELETE "//" natural "=" (* SSR plugin *) ] hat: [ | DELETE "^" "~" ident (* SSR plugin *) | DELETE "^" "~" natural (* SSR plugin *) ] ssriorpat: [ | ssripats OPT ( [ "|" | "|-" ] ssriorpat ) TAG SSR | DELETE OPT ssripats "|" ssriorpat (* SSR plugin *) | DELETE OPT ssripats "|-" ">" ssriorpat (* SSR plugin *) | DELETE OPT ssripats "|-" ssriorpat (* SSR plugin *) (* "|->" | "||" | "|||" | "||||" are parsing hacks *) | DELETE OPT ssripats "|->" ssriorpat (* SSR plugin *) | DELETE OPT ssripats "||" ssriorpat (* SSR plugin *) | DELETE OPT ssripats "|||" ssriorpat (* SSR plugin *) | DELETE OPT ssripats "||||" ssriorpat (* SSR plugin *) | DELETE OPT ssripats (* SSR plugin *) ] ssrbinder: [ | REPLACE "(" ssrbvar LIST1 ssrbvar ":" lconstr ")" (* SSR plugin *) | WITH "(" LIST1 ssrbvar ":" lconstr ")" TAG SSR | REPLACE "(" ssrbvar ":" lconstr ":=" lconstr ")" (* SSR plugin *) | WITH "(" ssrbvar OPT ( ":" lconstr ) OPT ( ":=" lconstr ) ")" TAG SSR | DELETE "(" ssrbvar ")" (* SSR plugin *) | DELETE "(" ssrbvar ":" lconstr ")" (* SSR plugin *) | DELETE "(" ssrbvar ":=" lconstr ")" (* SSR plugin *) ] ssrhavefwd: [ | REPLACE ":" ast_closure_lterm ":=" ast_closure_lterm (* SSR plugin *) | WITH ":" ast_closure_lterm ":=" OPT ast_closure_lterm TAG SSR | DELETE ":" ast_closure_lterm ":=" (* SSR plugin *) | DELETE ":=" ast_closure_lterm (* SSR plugin *) ] ssrmult_ne: [ | EDIT ADD_OPT natural ssrmmod TAG SSR ] rpattern: [ | REPLACE lconstr "in" lconstr "in" lconstr (* SSR plugin *) | WITH OPT ( OPT ( OPT ( OPT lconstr "in" ) lconstr ) "in" ) lconstr TAG SSR | DELETE lconstr (* SSR plugin *) | DELETE "in" lconstr (* SSR plugin *) | DELETE lconstr "in" lconstr (* SSR plugin *) | DELETE "in" lconstr "in" lconstr (* SSR plugin *) ] ssrrule_ne: [ | DELETE ssrsimpl_ne (* SSR plugin *) | REPLACE [ "/" ssrterm | ssrterm | ssrsimpl_ne ] (* SSR plugin *) | WITH [ OPT "/" ssrterm | ssrsimpl_ne ] TAG SSR ] ssrunlockarg: [ | REPLACE "{" ssrocc "}" ssrterm (* SSR plugin *) | WITH OPT ( "{" ssrocc "}" ) ssrterm TAG SSR | DELETE ssrterm (* SSR plugin *) ] ssrclauses: [ | REPLACE "in" ssrclausehyps "|-" "*" (* SSR plugin *) | WITH "in" ssrclausehyps OPT "|-" OPT "*" TAG SSR | DELETE "in" ssrclausehyps "|-" (* SSR plugin *) | DELETE "in" ssrclausehyps "*" (* SSR plugin *) | DELETE "in" ssrclausehyps (* SSR plugin *) | REPLACE "in" "|-" "*" (* SSR plugin *) | WITH "in" [ "*" | "*" "|-" | "|-" "*" ] TAG SSR | DELETE "in" "*" (* SSR plugin *) | DELETE "in" "*" "|-" (* SSR plugin *) ] ssrclausehyps: [ | REPLACE ssrwgen "," ssrclausehyps (* SSR plugin *) | WITH ssrwgen LIST0 ( OPT "," ssrwgen ) TAG SSR | DELETE ssrwgen ssrclausehyps (* SSR plugin *) | DELETE ssrwgen (* SSR plugin *) ] ssrwgen: [ | DELETE ssrhoi_hyp (* SSR plugin *) | REPLACE "@" ssrhoi_hyp (* SSR plugin *) | WITH OPT "@" ssrhoi_hyp TAG SSR | REPLACE "(" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) | WITH "(" ssrhoi_id OPT ( ":=" lcpattern ) ")" TAG SSR | DELETE "(" ssrhoi_id ")" (* SSR plugin *) | DELETE "(" "@" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) ] ssrcongrarg: [ | REPLACE natural constr ssrdgens (* SSR plugin *) | WITH OPT natural constr OPT ssrdgens TAG SSR | DELETE natural constr (* SSR plugin *) | DELETE constr ssrdgens (* SSR plugin *) | DELETE constr (* SSR plugin *) ] ssrviewpos: [ | DELETE "for" "apply" "/" "/" (* SSR plugin *) ] ssrhintref: [ | REPLACE constr "|" natural (* SSR plugin *) | WITH constr OPT ( "|" natural ) TAG SSR | DELETE constr (* SSR plugin *) ] ssr_search_arg: [ | REPLACE "-" ssr_search_item OPT ssr_search_arg (* SSR plugin *) | WITH LIST1 ( "-" ssr_search_item ) TAG SSR | DELETE ssr_search_item OPT ssr_search_arg (* SSR plugin *) ] ssr_search_item: [ | DELETE string (* SSR plugin *) | REPLACE string "%" preident (* SSR plugin *) | WITH string OPT ( "%" preident ) TAG SSR ] modloc: [ | REPLACE "-" global (* SSR plugin *) | WITH OPT "-" global TAG SSR | DELETE global ] ssrmmod: [ | DELETE LEFTQMARK (* SSR plugin *) (* duplicate *) ] clear_switch: [ | "{" LIST0 ident "}" ] ssrrwocc: [ | REPLACE "{" LIST0 ssrhyp "}" (* SSR plugin *) | WITH clear_switch ] ssrrwarg: [ | EDIT "{" ADD_OPT ssrocc "}" OPT ssrpattern_squarep ssrrule_ne TAG SSR | REPLACE "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne (* SSR plugin *) | WITH OPT ( OPT ( "{" LIST1 ssrhyp "}" ) ssrpattern_ne_squarep ) ssrrule_ne TAG SSR | DELETE ssrpattern_ne_squarep ssrrule_ne (* SSR plugin *) | DELETE ssrrule_ne (* SSR plugin *) ] ssrpattern_squarep: [ (* fix inconsistency *) | REPLACE "[" rpattern "]" (* SSR plugin *) | WITH ssrpattern_ne_squarep TAG SSR ] ssripats_ne: [ | REPLACE ssripat OPT ssripats (* SSR plugin *) | WITH LIST1 ssripat TAG SSR ] ssripats: [ (* fix inconsistency *) | REPLACE ssripat OPT ssripats (* SSR plugin *) | WITH ssripats_ne TAG SSR ] lcpattern: [ (* per @gares *) | DELETE "Qed" lconstr ] ssrapplyarg: [ | EDIT ADD_OPT ssrbwdview ":" ssragen OPT ssragens OPT ssrintros TAG SSR ] constr_with_bindings_arg: [ | EDIT ADD_OPT ">" constr_with_bindings ] destruction_arg: [ | DELETE constr_with_bindings ] ssrhintarg: [ | EDIT "[" ADD_OPT ssrortacs "]" TAG SSR ] ssrhint3arg: [ | EDIT "[" ADD_OPT ssrortacs "]" TAG SSR ] ssr_first: [ | DELETE ssr_first ssrintros_ne (* SSR plugin *) | REPLACE "[" LIST0 ltac_expr5 SEP "|" "]" (* SSR plugin *) | WITH "[" LIST0 ltac_expr5 SEP "|" "]" LIST0 ssrintros_ne TAG SSR ] ssr_first_else: [ | EDIT ssr_first ADD_OPT ssrorelse TAG SSR ] ssrseqarg: [ | EDIT ADD_OPT ssrseqidx ssrswap TAG SSR ] ssr_dpat: [ | REPLACE ssr_mpat "in" pattern200 ssr_rtype (* SSR plugin *) | WITH ssr_mpat OPT ( OPT ( "in" pattern200 ) ssr_rtype ) TAG SSR | DELETE ssr_mpat ssr_rtype (* SSR plugin *) | DELETE ssr_mpat (* SSR plugin *) ] ssr_one_term_pattern: [ | DELETE "Qed" constr ] ssrarg: [ | EDIT ADD_OPT ssrfwdview OPT ssreqid ssrdgens OPT ssrintros (* SSR plugin *) ] ssragen: [ | REPLACE "{" LIST1 ssrhyp "}" ssrterm (* SSR plugin *) | WITH OPT ( "{" LIST1 ssrhyp "}" ) ssrterm TAG SSR | DELETE ssrterm (* SSR plugin *) ] ssrbinder: [ | REPLACE [ "of" | "&" ] term99 (* SSR plugin *) | WITH "of" term99 TAG SSR | "&" term99 TAG SSR ] firstorder_rhs: [ | DELETE OPT firstorder_using | DELETE "with" LIST1 preident | REPLACE OPT firstorder_using "with" LIST1 preident | WITH OPT firstorder_using OPT ( "with" LIST1 preident ) ] attribute: [ | DELETE "using" OPT attr_value ] hypident: [ (* todo: restore for SSR *) | DELETE "(" "type" "of" ident ")" (* SSR plugin *) | DELETE "(" "value" "of" ident ")" (* SSR plugin *) ] ref_or_pattern_occ: [ | DELETE smart_global OPT occs | DELETE constr OPT occs | unfold_occ | pattern_occ ] clause_dft_concl: [ (* omit an OPT since clause_dft_concl is always OPT *) | REPLACE OPT occs | WITH occs ] simple_occurrences: [ | clause_dft_concl (* semantically restricted: no "at" clause *) ] occs_nums: [ | EDIT ADD_OPT "-" LIST1 nat_or_var ] variance_identref: [ | EDIT ADD_OPT variance identref ] conversion: [ | DELETE constr | DELETE constr "with" constr | REPLACE constr "at" occs_nums "with" constr | WITH OPT ( constr OPT ( "at" occs_nums ) "with" ) constr ] SPLICE: [ | clause | noedit_mode | match_list | match_context_list | IDENT | LEFTQMARK | NUMBER | STRING | hyp | 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 | term99 | term90 | term9 | term8 | pattern200 | pattern99 | pattern90 | ne_lstring | ne_string | lstring | fullyqualid | global | reference | bar_cbrace | lconstr (* SSR *) | ast_closure_term | ast_closure_lterm | ident_no_do | ssrterm | ssrtacarg | ssrtac3arg | ssrhyp | ssrhoi_hyp | ssrhoi_id | ssrhpats | ssrhpats_nobs | ssrfwdid | ssrmovearg | ssrcasearg | ssrrwargs | ssrviewposspc | ssrpatternarg | ssr_elsepat | ssr_mpat | ssrunlockargs | ssrcofixfwd | ssrfixfwd | ssrhavefwdwbinders | ssrparentacarg | ssrposefwd | ssrstruct | ssrrpat | ssrhint | ssrpattern_squarep | ssrhintref | ssr_search_item | ssr_modlocs | modloc | ssrexactarg | ssrclear | ssrmult | ssripats | ssrintros | ssrrule | ssrpattern_squarep | ssrcongrarg | ssrdotac | ssrunlockarg | ssr_search_arg | ssrortacarg | ssrsetfwd | ssr_idcomma | ssr_dthen | ssr_else | ssr_rtype | ssreqid | preident | lpar_id_coloneq | binders | casted_constr | check_module_types | decl_sep | function_fix_definition (* 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 | 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 | hint | 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 | 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 | ne_in_or_out_modules | search_queries | locatable | scope_delimiter | 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 | G_LTAC2_input_fun | ltac2_simple_intropattern_closed | ltac2_with_bindings | int_or_id | fun_ind_using | with_names | eauto_search_strategy_name | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) | number_string_mapping | number_options | string_option | tac2type_body | tac2rec_fields | mut_flag | tac2rec_fieldexprs | syn_level | firstorder_rhs | firstorder_using | hints_path_atom | ref_or_pattern_occ | cumul_ident_decl | variance | variance_identref | rewriter | conversion | type_cast ] (* end SPLICE *) RENAME: [ | occurrences rewrite_occs ] 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 *) | ltac_expr5 ltac_expr (* | nonsimple_intropattern intropattern (* ltac2 *) *) | term200 term | pattern100 pattern (*| impl_ident_tail impl_ident*) | ssexpr50 section_var_expr50 | ssexpr0 section_var_expr0 | section_subset_expr section_var_expr | fun_scheme_arg func_scheme_def | BULLET bullet | constr one_term (* many, many, many *) | class_rawexpr class (* OCaml reserved word *) | smart_global reference (* many, many *) (* | searchabout_query search_item *) | Pltac.tactic ltac_expr (* many uses in EXTENDs *) | ltac2_type5 ltac2_type | ltac2_expr6 ltac2_expr | starredidentref starred_ident_ref | ssrocc ssr_occurrences | ssrsimpl_ne s_item | ssrclear_ne ssrclear | ssrmult_ne mult | ssripats_ne ssripats | ssrrule_ne r_item | ssrintros_ne ssrintros | ssrpattern_ne_squarep ssrpattern_squarep | ssrrwarg rewrite_item | ssrrwocc occ_or_clear | rpattern rewrite_pattern | ssripat i_item | ssrwgen gen_item | ssrfwd ssrdefbody | ssrclauses ssr_in | ssrcpat ssrblockpat | constr_pattern one_pattern | hints_path hints_regexp | clause_dft_concl occurrences | in_clause goal_occurrences | unfold_occ reference_occs | pattern_occ pattern_occs | hypident_occ hyp_occs | concl_occ concl_occs | constr_with_bindings_arg one_term_with_bindings | red_flag reduction | strategy_flag reductions | delta_flag delta_reductions | q_strategy_flag q_reductions ] simple_tactic: [ (* due to renaming of tactic_value; Use LIST1 for function application *) | qualid LIST1 tactic_arg ] 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_decl 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_reductions | 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 ] REACHABLE: [ | NOTINRSTS ]