Quelle  common.edit_mlg   Sprache: unbekannt

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Defines additional productions and edits for use in documentation.  Not compiled into Coq *)

DOC_GRAMMAR

(* defined in ml *)
generic_tactic: [
| tactic
]

(* first, fixup symbols duplicated across files *)
lglob: [
| lconstr
| DELETE EXTRAARGS_lconstr
]

hint: [
| REPLACE "Resolve" "->" LIST1 global OPT natural
| WITH "Resolve" [ "->" | "<-" ] LIST1 global OPT natural
| DELETE "Resolve" "<-" LIST1 global OPT natural
| REPLACE "Variables" "Transparent"
| WITH [ "Constants" | "Projections" | "Variables" ] [ "Transparent" | "Opaque" ]
| DELETE "Variables" "Opaque"
| DELETE "Constants" "Transparent"
| DELETE "Constants" "Opaque"
| DELETE "Projections" "Transparent"
| DELETE "Projections" "Opaque"
| REPLACE "Transparent" LIST1 global
| WITH [ "Transparent" | "Opaque" ] LIST1 global
| DELETE "Opaque" LIST1 global

| REPLACE "Extern" natural OPT Constr.constr_pattern "=>" generic_tactic
| WITH "Extern" natural OPT constr_pattern "=>" generic_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 Procq.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_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
]

(* Renames to eliminate qualified names.
   Put other renames at the end *)
RENAME: [
  (* map missing names for rhs *)
| Constr.constr term
| Constr.term0 term0
| Constr.global global
| Constr.lconstr lconstr
| Constr.cpattern cpattern
| 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
| Pltac.ltac_expr ltac_expr5

(*
| G_vernac.def_body def_body
| Prim.by_notation by_notation
| Prim.natural natural
*)
| Vernac.fix_definition fix_definition
]

(* 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_nat_coloneq
| 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
| test_qualid_with_or_lpar_or_rbrac
| test_leftsquarebracket_equal
| test_old_sort_qvar
| test_sort_qvar
| test_ltac2_ident
| test_doublepipe_univ_decl
| test_doublepipe_cumul_univ_decl
| test_semicolon_cumul_univ_decl
]

(* 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
]

qualid: [ | DELETENT ]

qualid: [
| ident LIST0 ("." 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 ]
]

type: [
| term200
]

one_type: [
| constr
]

term_forall_or_fun: [
| "forall" open_binders "," type
]

binder_constr: [
| DELETE "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_if "if" term200 as_return_type "then" term200 "else" term200
| 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
]

qualid_annotated: [
| global univ_annot
]

atomic_constr: [
| qualid_annotated
| 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 "]"
]

(* lexer token *)
IDENT: [
| ident
]

scope_key: [
| IDENT
]

scope_name: [
| IDENT
]

scope: [
| scope_name
| scope_key
]

scope_delimiter: [
| REPLACE "%" IDENT
| WITH "%" scope
| REPLACE "%_" IDENT
| WITH "%_" scope
]

sort: [
| REPLACE "Type" "@{" reference ";" universe "}"
| WITH "Type" "@{" OPT [ qualid [ "|" | ";" ] ] universe "}"
| DELETE "Type" "@{" universe "}"
| DELETE "Type" "@{" reference "|" universe "}"
]

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
| 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 univ_annot LIST0 arg ")"
| WITH    term0 ".(" global univ_annot LIST0 arg ")" (* huh? *)
| REPLACE term0 "%" IDENT
| WITH term0 "%" scope_key
| MOVETO term_scope term0 "%" scope_key
| REPLACE term0 "%_" IDENT
| WITH term0 "%_" scope_key
| MOVETO term_scope term0 "%_" scope_key
| MOVETO term_projection term0 ".(" global univ_annot LIST0 arg ")"
| MOVETO term_projection term0 ".(" "@" global univ_annot LIST0 ( term9 ) ")"
]

term0: [
| DELETE reference univ_annot
| REPLACE "{|" record_declaration bar_cbrace
| WITH "{|" OPT [ LIST1 field_def SEP ";" OPT ";" ] bar_cbrace
| MOVETO number_or_string NUMBER
| MOVETO number_or_string string
| MOVETO term_record "{|" OPT [ LIST1 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 "(" name ":" lconstr "|" lconstr ")"
| WITH "(" name ":" type "|" lconstr ")"

| MOVETO generalizing_binder "`(" LIST1 typeclass_constraint SEP "," ")"
| MOVETO generalizing_binder "`{" LIST1 typeclass_constraint SEP "," "}"
| MOVETO generalizing_binder "`[" LIST1 typeclass_constraint SEP "," "]"
]

(* next two used internally  for declaring notations *)
one_closed_binder: [
| DELETENT
]

one_open_binder: [
| DELETENT
]

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
| 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 "}" OPT [ "as" identref ] )
]

(* No mixed inductive-record definitions, opt_coercion is meaningless for Inductive *)
inductive_definition: [
| cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] ":=" OPT [ OPT "|" LIST1 constructor SEP "|" ] decl_notations
]

(* No mutual recursion, no inductive classes, type must be a sort *)
(* constructor is optional but "Class record_definition" covers that case *)
singleton_class_definition: [
| 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 [ 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
| DELETE "Symbols" assum_list
| REPLACE "Symbol" assum_list
| WITH [ "Symbol" | "Symbols" ] assum_list
| REPLACE inductive_token LIST1 inductive_or_record_definition SEP "with"
| WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
|   "Inductive" record_definition LIST0 ( "with" record_definition )
|   "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
|   "CoInductive" record_definition LIST0 ( "with" record_definition )
| REPLACE finite_token inductive_or_record_definition
| WITH "Variant" variant_definition
|   [ "Record" | "Structure" ] 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 )
| DELETE "Scheme" "Boolean" "Equality" "for" smart_global
| DELETE "Scheme" "Equality" "for" smart_global
| "Scheme" OPT "Boolean" "Equality" "for" smart_global
| DELETE "Rewrite" "Rules" identref ":=" OPT "|" LIST1 rewrite_rule SEP "|"
| REPLACE "Rewrite" "Rule" identref ":=" OPT "|" LIST1 rewrite_rule SEP "|"
| WITH "Rewrite" [ "Rule" | "Rules" ]  identref ":=" OPT "|" LIST1 rewrite_rule SEP "|"
]

SPLICE: [
| variant_definition
]

finite_token: [
| DELETENT
]

inductive_token: [
| DELETENT
]

inductive_or_record_definition: [
| DELETENT
]

constructors_or_record: [
| DELETENT
]

record_fields: [
| REPLACE record_field ";" record_fields
| WITH OPT [ LIST1 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 identref [ "+" | ] univ_decl_constraints
| WITH    "@{" OPT [ LIST0 identref [ "|" | ";" ] ] LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
| DELETE "@{" LIST0 identref [ "+" | ] univ_decl_constraints
| DELETE "@{" LIST0 identref "|" LIST0 identref [ "+" | ] univ_decl_constraints
]

cumul_univ_decl: [
| REPLACE "@{" LIST0 identref ";" LIST0 variance_identref [ "+" | ] univ_decl_constraints
| WITH "@{" OPT [ LIST0 identref [ "|" | ";" ] ] LIST0 variance_identref    OPT "+"   OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
| DELETE "@{" LIST0 variance_identref [ "+" | ] univ_decl_constraints
| DELETE "@{" LIST0 identref "|" LIST0 variance_identref [ "+" | ] univ_decl_constraints
]

of_type: [
| DELETENT
]

of_type: [
| [ ":" | ":>" ] type
]

of_type_inst: [
| DELETENT
]

of_type_inst: [
| [ ":" | ":>" | "::" | "::>" ] 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 "head" OPT delta_flag
| WITH OPT "head" 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 ":" coercion_class ">->" coercion_class
| REPLACE "Coercion" by_notation ":" coercion_class ">->" coercion_class
| WITH "Coercion" smart_global OPT [ ":" coercion_class ">->" coercion_class ]

(* semantically restricted per https://github.com/coq/coq/pull/12936#discussion_r492705820 *)
(* global OPT univ_decl is just ident_decl, the first OPT is moved to the rule above *)
| REPLACE "Coercion" global OPT [ OPT univ_decl def_body ]
| WITH "Coercion" ident_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 *)
| DELETE "Export" "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 ]

| DELETE "Require" export_token LIST1 filtered_import
| REPLACE "From" global "Require" export_token LIST1 filtered_import
| WITH OPT [ "From" dirpath ] "Require" export_token LIST1 filtered_import

| REPLACE "From" global "Extra" "Dependency" ne_string OPT [ "as" IDENT ]
| WITH "From" dirpath "Extra" "Dependency" ne_string OPT [ "as" IDENT ]
]

export_token: [
| REPLACE "Import" OPT import_categories
| WITH [ "Import" | "Export" ] OPT import_categories
| DELETE "Export" OPT import_categories
]

(* 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 ]
]

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
| 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_constructs: [
(* repeated in main ltac grammar - need to create a COPY edit *)
| ltac_expr3 ";" [ ltac_expr3 ]
| ltac_expr3 ";" "[" for_each_goal "]"

| ltac_expr1 "+" [ ltac_expr2 ]
| ltac_expr1 "||" [ ltac_expr2 ]

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

l3_tactic: [ ]

ltac_expr3: [
| DELETE "abstract" ltac_expr2
| REPLACE "abstract" ltac_expr2 "using" ident
| WITH "abstract" ltac_expr2 OPT ( "using" ident )
| l3_tactic
| MOVEALLBUT ltac_builtins
| l3_tactic
| ltac_expr2
]

l2_tactic: [ ]

ltac_expr2: [
| MOVETO ltac_builtins "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2
| l2_tactic
| DELETE ltac_builtins
]

l1_tactic: [ ]

ltac_expr1: [
| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5
| 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
]

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 "assert" "(" identref ":" lconstr ")" by_tactic
| WITH "assert" "(" identref ":" type ")" by_tactic
| REPLACE "assert" constr as_ipat by_tactic
| WITH "assert" one_type as_ipat by_tactic
| REPLACE "eassert" "(" identref ":" lconstr ")" by_tactic
| WITH "eassert" "(" identref ":" type ")" by_tactic
| REPLACE "eassert" constr as_ipat by_tactic
| WITH "eassert" one_type as_ipat by_tactic
| REPLACE "cut" constr
| WITH "cut" one_type
| REPLACE "evar" constr
| WITH "evar" one_type
| REPLACE "absurd" constr
| WITH "absurd" one_type
| REPLACE "enough" "(" identref ":" lconstr ")" by_tactic
| WITH "enough" "(" identref ":" type ")" by_tactic
| REPLACE "enough" constr as_ipat by_tactic
| WITH "enough" one_type as_ipat by_tactic
| REPLACE "eenough" "(" identref ":" lconstr ")" by_tactic
| WITH "eenough" "(" identref ":" type ")" by_tactic
| REPLACE "eenough" constr as_ipat by_tactic
| WITH "eenough" one_type as_ipat by_tactic
| 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 "head" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
| WITH "simpl" OPT "head" 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
| 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 "clear" LIST0 hyp
| REPLACE "clear" "-" LIST1 hyp
| WITH "clear" OPT ( OPT "-" LIST1 hyp )
| 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" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" constr ]
| "dependent" "inversion" quantified_hypothesis as_or_and_ipat OPT [ "with" constr ]
| "dependent" "simple" "inversion" quantified_hypothesis as_or_and_ipat OPT [ "with" constr ]
| "dependent" "inversion_clear" quantified_hypothesis as_or_and_ipat OPT [ "with" constr ]
| 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" LIST1 constr
| REPLACE "generalize" constr occs as_name LIST0 [ "," pattern_occ as_name ]
| WITH "generalize" LIST1 [ pattern_occ as_name ] SEP ","
| REPLACE "evar" "(" ident ":" lconstr ")"
| WITH "evar" "(" ident ":" type ")"
| 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 where
| REPLACE "refine" uconstr
| WITH OPT "simple" OPT "notypeclasses" "refine" uconstr
| DELETE "simple" "refine" uconstr
| DELETE "notypeclasses" "refine" uconstr
| DELETE "simple" "notypeclasses" "refine" uconstr
| DELETE "replace" "->" uconstr clause
| DELETE "replace" "<-" uconstr clause
| DELETE "replace" uconstr clause
| "replace" orient uconstr clause
| REPLACE "replace" uconstr "with" constr clause by_arg_tac
| WITH "replace" orient constr "with" constr clause OPT ( "by" ltac_expr3 )
| DELETE "replace" "->" uconstr "with" constr clause by_arg_tac
| DELETE "replace" "<-" uconstr "with" constr clause by_arg_tac
| 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 "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 simple_occurrences
| 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 as_ipat
| DELETE "exists"
| REPLACE "exists" LIST1 bindings SEP ","
| WITH "exists" LIST0 bindings SEP ","
| DELETE "eexists"
| REPLACE "eexists" LIST1 bindings SEP ","
| WITH "eexists" LIST0 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 "subst" LIST1 hyp
| WITH "subst" LIST0 hyp
| DELETE "subst"
| DELETE "congruence" OPT natural
| REPLACE "congruence" OPT natural "with" LIST1 constr
| WITH "congruence" OPT natural OPT ( "with" LIST1 constr )
| DELETE "simple" "congruence" OPT natural
| REPLACE "simple" "congruence" OPT natural "with" LIST1 constr
| WITH "simple" "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" | "dfs" | "best_effort" ] OPT nat_or_var OPT ( "with" LIST1 preident )
| DELETE "typeclasses" "eauto" "dfs" OPT nat_or_var "with" LIST1 preident
| DELETE "typeclasses" "eauto" "dfs" OPT nat_or_var
| DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident
| DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var
| DELETE "typeclasses" "eauto" "best_effort" OPT nat_or_var "with" LIST1 preident
| DELETE "typeclasses" "eauto" "best_effort" OPT nat_or_var
| DELETE "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident
| DELETE "typeclasses" "eauto" OPT nat_or_var
(* first/solve variants defined with register_list_tactical in coretactics.mlg *)
| "first" ident
| "solve" ident
(* 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 )
]

(* todo: don't use DELETENT for this *)
ne_intropatterns: [ | DELETENT ]

or_and_intropattern: [
| REPLACE "[" LIST1 intropatterns SEP "|" "]"
| WITH "[" LIST0 (LIST0 intropattern) SEP "|" "]"
| DELETE "()"
| DELETE "(" simple_intropattern ")"
| REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
|   WITH  "(" LIST0 simple_intropattern SEP "," ")"
  (* makes the grammar a little ambiguous for "()" and "( simple_intropattern )"
     but semantically doesn't matter *)
| REPLACE "(" simple_intropattern "&" LIST1 simple_intropattern SEP "&" ")"
|   WITH  "(" LIST0 simple_intropattern SEP "&" ")"
]

equality_intropattern: [
| REPLACE "[" "=" intropatterns "]"
| WITH    "[=" intropatterns "]"
]

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 [ [ "With" | "Without" ] "Constraint" "Sources" ] OPT ne_string
| WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT [ [ "With" | "Without" ] "Constraint" "Sources" ] 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" "*"
| DELETE "Notation" string
| REPLACE "Notation" string "in" "custom" IDENT
| WITH "Notation" string OPT [ "in" "custom" IDENT ]

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

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 "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" identref
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" identref
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" identref
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" identref
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr OPT ( "reflexivity" "proved" "by" constr ) OPT ( "symmetry" "proved" "by" constr ) OPT ("transitivity" "proved" "by" constr ) "as" identref
| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" identref
| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" identref
| DELETE "Add" "Relation" constr constr "as" identref
| DELETE "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" identref
| DELETE "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| DELETE "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| DELETE "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Relation" constr constr OPT ( "reflexivity" "proved" "by" constr ) OPT ( "symmetry" "proved" "by" constr ) OPT ( "transitivity" "proved" "by" constr ) "as" identref
| REPLACE "Admit" "Obligations" "of" identref
| WITH "Admit" "Obligations" OPT ( "of" identref )
| 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" identref "with" constr "Sort" sort_quality_or_set
| WITH "Derive" "Inversion" identref "with" constr OPT ( "Sort" sort_quality_or_set )
| DELETE "Derive" "Inversion" identref "with" constr
| REPLACE "Derive" "Inversion_clear" identref "with" constr "Sort" sort_quality_or_set
| WITH "Derive" "Inversion_clear" identref "with" constr OPT ( "Sort" sort_quality_or_set )
| DELETE "Derive" "Inversion_clear" identref "with" constr
| EDIT "Focus" ADD_OPT natural
| DELETE "Hint" "Rewrite" orient LIST1 constr ":" LIST1 preident
| REPLACE "Hint" "Rewrite" orient LIST1 constr "using" generic_tactic ":" LIST1 preident
| WITH "Hint" "Rewrite" orient LIST1 constr OPT ( "using" generic_tactic ) OPT ( ":" LIST1 preident )
| DELETE "Hint" "Rewrite" orient LIST1 constr
| DELETE "Hint" "Rewrite" orient LIST1 constr "using" generic_tactic
| REPLACE "Next" "Obligation" "of" identref withtac
| WITH "Next" "Obligation" OPT ( "of" identref ) withtac
| DELETE "Next" "Obligation" withtac
| REPLACE "Final" "Obligation" "of" identref withtac
| WITH "Final" "Obligation" OPT ( "of" identref ) withtac
| DELETE "Final" "Obligation" withtac
| REPLACE "Obligation" natural "of" identref withtac
| WITH "Obligation" natural OPT ( "of" identref ) withtac
| DELETE "Obligation" natural withtac
| REPLACE "Obligations" "of" identref
| WITH "Obligations" OPT ( "of" identref )
| DELETE "Obligations"
| REPLACE "Preterm" "of" identref
| WITH "Preterm" OPT ( "of" identref )
| DELETE "Preterm"
| REPLACE "Proof" "using" section_var_expr "with" generic_tactic
| WITH "Proof" "using" section_subset_expr OPT [ "with" generic_tactic ]
| 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

(* hide special case command that looks like a "Set" command *)
| DELETE "Set" "Firstorder" "Solver" generic_tactic

| 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" withtac
| WITH "Solve" "All" "Obligations" OPT ( "with" tactic )
| REPLACE "Solve" "Obligations" "of" identref withtac
| WITH "Solve" "Obligations" OPT ( "of" identref ) OPT ( "with" tactic )
| DELETE "Solve" "Obligations" withtac
| DELETE "Undo"
| DELETE "Undo" natural
| REPLACE "Undo" "To" natural
| WITH "Undo" OPT ( OPT "To" natural )
| DELETE "Abort" "All"
| REPLACE "Abort"
| WITH "Abort" OPT [ "All" ]

(* 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

| REPLACE "Derive" open_binders "SuchThat" constr "As" identref      (* derive plugin *)
| WITH "Derive" open_binders "SuchThat" type "As" ident      (* derive plugin *)

| REPLACE "Derive" open_binders "in" constr "as" identref      (* derive plugin *)
| WITH "Derive" open_binders "in" type "as" ident      (* derive plugin *)

(* odd that these are in command while other notation-related ones are in syntax *)
| REPLACE "Number" "Notation" reference reference reference OPT number_options ":" preident
| WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name
| REPLACE "String" "Notation" reference reference reference OPT string_option ":" preident
| WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name

| DELETE "Ltac2" ltac2_entry      (* was split up *)
| DELETE "Add" "Zify" "InjTyp" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "BinOp" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "UnOp" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "CstOp" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "BinRel" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "PropOp" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "PropBinOp" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "PropUOp" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "BinOpSpec" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "UnOpSpec" reference      (* micromega plugin *)
| DELETE "Add" "Zify" "Saturate" reference      (* micromega plugin *)
| "Add" "Zify" add_zify reference  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 coercion_class
| WITH "Bind" "Scope" scope_name; "with" LIST1 coercion_class
]

opt_scope: [
| REPLACE ":" IDENT
| WITH    ":" scope_name
]

syntax_modifier: [
| DELETE "in" "custom" IDENT
| REPLACE "in" "custom" IDENT; "at" "level" natural
| WITH "in" "custom" IDENT OPT ( "at" "level" natural )
| DELETE IDENT; "in" "scope" IDENT
| REPLACE IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
| WITH LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
]

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 *)
]

field_body: [
| REPLACE binders of_type_inst lconstr
| WITH binders of_type_inst
| REPLACE binders of_type_inst lconstr ":=" lconstr
| WITH binders of_type_inst ":=" lconstr
]

assum_list: [
| DELETE LIST1 assum_coe
| LIST1 assum_coe
]

assumpt: [
| REPLACE LIST1 ident_decl of_type lconstr
| WITH LIST1 ident_decl of_type
]

constructor_type: [
| REPLACE binders [ of_type_inst lconstr | ]
| WITH binders OPT of_type_inst
]

(* 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
]

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 "Instructions" vernac_control
| WITH "Instructions" sentence
| REPLACE "Profile" OPT STRING vernac_control
| WITH "Profile" OPT STRING 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
| REPLACE "Succeed" vernac_control
| WITH "Succeed" 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 *)
]

record_declaration: [
| DELETE fields_def
| LIST0 field_def
]

fields_def: [ | DELETENT ]

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 notation_declaration SEP decl_sep
| WITH "where" notation_declaration LIST0 (decl_sep notation_declaration )
]

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" | "in" | "outside" ] LIST1 global
| DELETE "in" 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_key )
| 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 ]
]

notation_declaration: [
| REPLACE lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
| WITH 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
]

subprf_with_selector: [
| DELETE query_command
]

SPLICE: [
| subprf_with_selector
]

tactic_mode: [
(* todo: make sure to document this production! *)
(* deleting to allow splicing query_command into 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
| MOVETO simple_tactic subprf
| REPLACE OPT toplevel_selector "{"
(* semantically restricted *)
| WITH OPT ( [ natural | "[" ident "]" ] ":" ) "{"
| MOVETO simple_tactic OPT ( [ natural | "[" ident "]" ] ":" ) "{"
| DELETE command
| DELETENT
]

SPLICE: [
| subprf
]

ltac2_syntax_class: [
| REPLACE syn_node      (* Ltac2 plugin *)
| WITH name TAG Ltac2
| REPLACE syn_node "(" LIST1 ltac2_syntax_class SEP "," ")"      (* Ltac2 plugin *)
| WITH name "(" LIST1 ltac2_syntax_class SEP "," ")" TAG Ltac2
]

tac2mode: [
| DELETENT
]

(* not sure how this is used *)
tac2expr_in_env: [
| DELETENT
]

syn_node: [ | DELETENT ]

RENAME: [
| toplevel_selector toplevel_selector_temp
]

toplevel_selector: [
| goal_selector
| "all"
| "!"
(* par is accepted even though it's not in the .mlg *)
| "par"
]

toplevel_selector_temp: [
| DELETE goal_selector ":"
| DELETE "all" ":"
| DELETE "!" ":"
| toplevel_selector ":"
]

(* not included in insertprodn; defined in rst with :production: *)
control_command: [ ]

(* move all commands under "command" *)

vernac_aux: [
| DELETE gallina "."
| DELETE gallina_ext "."
| DELETE syntax "."
| DELETE command_entry
| DELETENT
]

command: [
| gallina
| gallina_ext
| syntax
| query_command
| vernac_control
| vernac_toplevel
]

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: [
| "case_eq" constr
(* | "case_eq" induction_clause_list ??? *)
| "classical_left"
| "classical_right"
| "contradict" ident
| "easy"
| "inversion_sigma" OPT ( ident OPT ( "as" simple_intropattern ) )
| "lia"
| "lra"
| "nia"
| "now_show" one_type
| "nra"
| "rapply" constr
| "tauto"
| "time_constr" ltac_expr5
| "zify"
]

(* todo: need careful review; assume that "[" ... "]" are literals *)
tactic_notation_tactics: [
| "assert_fails" ltac_expr3
| "clear" "dependent" hyp
| "decide" constr "with" constr
| "dependent" "destruction" ident OPT ( "generalizing" LIST1 hyp )  OPT ( "using" constr )
| "dependent" "induction" ident OPT ( [ "generalizing" | "in" ] LIST1 hyp )  OPT ( "using" constr )
| "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
| "revert" "dependent" hyp
| "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: [
| 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"
| DELETE "Symbol"
(* SubClass was deleted from def_token *)
| [ "Definition" | "Example" | "Context" | "Primitive" | "Symbol" ]
| DELETE "Coercion"
| DELETE "Instance"
| DELETE "Scheme"
| DELETE "Canonical"
| [  "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
| DELETE "Fixpoint"
| DELETE "CoFixpoint"
| DELETE "Field"
| DELETE "Method"
| [  "Fixpoint" | "CoFixpoint" | "Field" | "Method" ]
]

(* ltac2 *)

DELETE: [
| test_ltac1_env
]

rec_flag: [
| OPTINREF
]

q_orient: [
| DELETE "<-"
| REPLACE "->"
| WITH 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 SEP ";" 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_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" ident ":=" 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
]

ltac2_equality_intropattern: [
| REPLACE "[" "=" ltac2_intropatterns "]"
| WITH    "[=" ltac2_intropatterns "]"
]

SPLICE: [
| tac2def_val
| tac2def_typ
| tac2def_ext
| tac2def_syn
| ltac2def_syn
| tac2def_mut
| rec_flag
| tac2alg_constructors
| ltac2_binder
| branch
| anti
| array_literal
| list_literal
]

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_atom: [
| MOVETO ltac2_quotations "constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
| MOVETO ltac2_quotations "open_constr" ":" "(" lconstr ")"      (* Ltac2 plugin *)
| MOVETO ltac2_quotations "preterm" ":" "(" lconstr ")"      (* Ltac2 plugin *)
| MOVETO ltac2_quotations "ident" ":" "(" identref ")"      (* 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: [
--> --------------------

--> maximum size reached

--> --------------------