(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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

(* renames to eliminate qualified names
   put other renames at the end *)
RENAME: [
  (* map missing names for rhs *)
| Constr.constr term
| Constr.constr_pattern constr_pattern
| Constr.global global
| Constr.lconstr lconstr
| Constr.lconstr_pattern lconstr_pattern
| G_vernac.query_command query_command
| G_vernac.section_subset_expr section_subset_expr
| Pltac.tactic tactic
| Pltac.tactic_expr tactic_expr5
| Prim.ident ident
| Prim.reference reference
| Pvernac.Vernac_.main_entry vernac_control
| Tactic.tactic tactic

  (* SSR *)
(*
| G_vernac.def_body def_body
| Pcoq.Constr.constr term
| Prim.by_notation by_notation
| Prim.identref ident
| Prim.natural natural
*)
| Vernac.rec_definition rec_definition
(* todo: hmm, rename adds 1 prodn to closed_binder?? *)
| Constr.closed_binder closed_binder
]

(* written in OCaml *)
impl_ident_head: [
| "{" ident
]

lpar_id_coloneq: [
| "(" ident; ":="
]

(* lookahead symbols *)
DELETE: [
| check_for_coloneq
| local_test_lpar_id_colon
| lookup_at_as_comma
| test_only_starredidentrefs
| test_bracket_ident
| test_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

  (* SSR *)
(* | ssr_null_entry *)
(*
| ssrtermkind  (* todo: rename as "test..." *)
| term_annotation  (* todo: rename as "test..." *)
| test_idcomma
| test_nohidden
| test_not_ssrslashnum
| test_ssr_rw_syntax
| test_ssreqid
| test_ssrfwdid
| test_ssrseqvar
| test_ssrslashnum00
| test_ssrslashnum01
| test_ssrslashnum10
| test_ssrslashnum11
| test_ident_no_do
| ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
| ssrseqdir
*)

(* unused *)
| constr_comma_sequence'
| auto_using'
| constr_may_eval
]

(* ssrintrosarg: [ | DELETENT ] *)

(* additional nts to be spliced *)

hyp: [
| var
]

ltac_expr_opt: [
| OPT tactic_expr5
]

ltac_expr_opt_list_or: [
| ltac_expr_opt_list_or "|" ltac_expr_opt
| ltac_expr_opt
]

tactic_then_gen: [
| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
| REPLACE OPT tactic_expr5 ".." tactic_then_last
| WITH ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
]

ltac_expr_opt_list_or: [
| ltac_expr_opt_list_or "|" OPT tactic_expr5
| OPT tactic_expr5
]

reference: [ | DELETENT ]

reference: [
| qualid
]

fullyqualid: [ | DELETENT ]

fullyqualid: [
| qualid
]

field_ident: [
| "." ident
]

basequalid: [
| REPLACE ident fields
| WITH ident LIST0 field_ident
| DELETE ident
]

field: [ | DELETENT ]
fields: [ | DELETENT ]

dirpath: [
| REPLACE ident LIST0 field
| WITH ident
| dirpath field_ident
]

binders: [
| DELETE Pcoq.Constr.binders  (* todo: not sure why there are 2 "binders:" *)
]

lconstr: [
| DELETE l_constr
]


let_type_cstr: [
| DELETE OPT [ ":" lconstr ]
| type_cstr
]

(* rename here because we want to use "return_type" for something else *)
RENAME: [
| return_type as_return_type
]

case_item: [
| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
| WITH operconstr100 OPT ("as" name) OPT [ "in" pattern200 ]
]

binder_constr: [
| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
| MOVETO term_fix "let" "fix" fix_decl "in" operconstr200
| MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200
| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
| MOVETO term_fix "fix" fix_decls
| MOVETO term_cofix "cofix" cofix_decls
]

term_let: [
| REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
| WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200
| "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200
(* Don't need to document that "( )" is equivalent to "()" *)
| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" operconstr200 "in" operconstr200
| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" operconstr200 "in" operconstr200
| REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
| WITH  "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200
| DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
]

atomic_constr: [
(* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
(* | DELETE string *)
| REPLACE "?" "[" ident "]"
| WITH "?[" ident "]"
| MOVETO term_evar "?[" ident "]"
| REPLACE "?" "[" pattern_ident "]"
| WITH "?[" pattern_ident "]"
| MOVETO term_evar "?[" pattern_ident "]"
| MOVETO term_evar pattern_ident evar_instance
]

tactic_expr0: [
| REPLACE "[" ">" tactic_then_gen "]"
| WITH "[>" tactic_then_gen "]"
]

operconstr100: [
| MOVETO term_cast operconstr99 "<:" operconstr200
| MOVETO term_cast operconstr99 "<<:" operconstr200
| MOVETO term_cast operconstr99 ":" operconstr200
| MOVETO term_cast operconstr99 ":>"
]

operconstr10: [
(* fixme: add in as a prodn somewhere *)
| MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
| DELETE dangling_pattern_extension_rule
]

operconstr9: [
(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
| DELETE ".." operconstr0 ".."
]

operconstr1: [
| REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
| WITH operconstr0 ".(" global LIST0 appl_arg ")"
| MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
]

operconstr0: [
(* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
| DELETE "{" binder_constr "}"
| REPLACE "{|" record_declaration bar_cbrace
| WITH "{|" LIST0 field_def bar_cbrace
]

fix_decls: [
| DELETE fix_decl
| REPLACE fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
| WITH fix_decl OPT ( LIST1 ("with" fix_decl) "for" identref )
]

cofix_decls: [
| DELETE cofix_decl
| REPLACE cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref
| WITH cofix_decl OPT ( LIST1 ( "with" cofix_decl ) "for" identref )
]

fields_def: [
| REPLACE field_def ";" fields_def
| WITH LIST1 field_def SEP ";"
| DELETE field_def
]

binders_fixannot: [
| DELETE binder binders_fixannot
| DELETE fixannot
| DELETE (* empty *)
| LIST0 binder OPT fixannot
]

binder: [
| DELETE name
]

open_binders: [
| REPLACE name LIST0 name ":" lconstr
| WITH LIST1 name ":" lconstr
(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
| DELETE name ".." name
| REPLACE name LIST0 name binders
| WITH LIST1 binder
| DELETE closed_binder binders
]

type: [
| operconstr200
]

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  "}"

| DELETE "[" name "]"
| DELETE "[" name LIST1 name "]"

| REPLACE "[" name LIST1 name ":" lconstr "]"
| WITH "[" LIST1 name type_cstr "]"
| DELETE "[" name ":" lconstr  "]"

| REPLACE "(" Prim.name ":" lconstr "|" lconstr ")"
| WITH "(" Prim.name ":" type "|" lconstr ")"
]

name_colon: [
| name ":"
]

typeclass_constraint: [
| EDIT ADD_OPT "!" operconstr200
| REPLACE "{" name "}" ":" [ "!" | ] operconstr200
| WITH "{" name "}" ":" OPT "!"  operconstr200
| REPLACE name ":" [ "!" | ] operconstr200
| WITH name ":" OPT "!" operconstr200
]

(* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
Prim.name: [
| REPLACE "_"
| WITH name
]

oriented_rewriter: [
| REPLACE orient_rw rewriter
| WITH orient rewriter
]

DELETE: [
| orient_rw
]

pattern10: [
| REPLACE pattern1 LIST1 pattern1
| WITH pattern1 LIST0 pattern1
| DELETE pattern1
]

pattern0: [
| REPLACE "(" pattern200 ")"
| WITH "(" LIST1 pattern200 SEP "|" ")"
| DELETE "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
| REPLACE "{|" record_patterns bar_cbrace
| WITH "{|" LIST0 record_pattern bar_cbrace
]

DELETE: [
| record_patterns
]

eqn: [
| REPLACE LIST1 mult_pattern SEP "|" "=>" lconstr
| WITH LIST1 [ LIST1 pattern100 SEP "," ] SEP "|" "=>" lconstr
]

universe_increment: [
| OPTINREF
]

evar_instance: [
| OPTINREF
]

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 OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
| WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
|   "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
|   "Variant" inductive_definition LIST0 ( "with" inductive_definition )
|   [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition )
|   "Class" inductive_definition LIST0 ( "with" inductive_definition )
| REPLACE "Fixpoint" LIST1 rec_definition SEP "with"
| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with"
| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition )
| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with"
| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with"
| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
| REPLACE "Scheme" LIST1 scheme SEP "with"
| WITH "Scheme" scheme LIST0 ( "with" scheme )
]

DELETE: [
| private_token
| cumulativity_token
]

constructor_list_or_record_decl: [
| OPTINREF
]

record_fields: [
| REPLACE record_field ";" record_fields
| WITH LIST1 record_field SEP ";"
| DELETE record_field
| DELETE (* empty *)
]

assumptions_token: [
| DELETENT
]

inline: [
| REPLACE "Inline" "(" natural ")"
| WITH "Inline" OPT ( "(" natural ")" )
| DELETE "Inline"
| OPTINREF
]

univ_instance: [
| OPTINREF
]

univ_decl: [
| REPLACE "@{" LIST0 identref [ "+" | ]     [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
| WITH    "@{" LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
]

of_type_with_opt_coercion: [
| DELETENT
]

of_type_with_opt_coercion: [
| [ ":" | ":>" | ":>>" ] type
]

attribute_value: [
| OPTINREF
]

def_body: [
| DELETE binders ":=" reduce lconstr
| REPLACE binders ":" lconstr ":=" reduce lconstr
| WITH LIST0 binder OPT (":" type) ":=" reduce lconstr
| REPLACE binders ":" lconstr
| WITH LIST0 binder ":" type
]

reduce: [
| OPTINREF
]

occs: [
| OPTINREF
]

delta_flag: [
| REPLACE "-" "[" LIST1 smart_global "]"
| WITH OPT "-" "[" LIST1 smart_global "]"
| DELETE "[" LIST1 smart_global "]"
| OPTINREF
]

strategy_flag: [
| REPLACE OPT delta_flag
| WITH delta_flag
| (* empty *)
| OPTINREF
]

export_token: [
| OPTINREF
]

functor_app_annot: [
| OPTINREF
]

is_module_expr: [
| OPTINREF
]

is_module_type: [
| OPTINREF
]

gallina_ext: [
| REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
| WITH "Arguments" smart_global LIST0 argument_spec_block    LIST0 [  "," LIST0 more_implicits_block ]                OPT [ ":" LIST1 arguments_modifier SEP "," ]
]

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

integer: [ | DELETENT ]
RENAME: [
| integer int (* todo: review uses in .mlg files, some should be "natural" *)
]

LEFTQMARK: [
| "?"
]

digit: [
| "0" ".." "9"
]

num: [
| LIST1 digit
]

natural: [ | DELETENT ]
natural: [
| num  (* todo: or should it be "nat"? *)
]

numeral: [
| LIST1 digit OPT ("." LIST1 digit) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
]

int: [
| OPT "-" LIST1 digit
]

bigint: [
| DELETE NUMERAL
| num
]

first_letter: [
| [ "a" ".." "z" | "A" ".." "Z" | "_" | unicode_letter ]
]

subsequent_letter: [
| [ first_letter | digit | "'" | unicode_id_part ]
]

ident: [
| DELETE IDENT
| first_letter LIST0 subsequent_letter
]

NUMERAL: [
| numeral
]

(* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *)

string: [ | DELETENT ]
STRING: [
| string
]


(* todo: is "bigint" useful?? *)
(* todo: "check_int" in g_prim.mlg should be "check_num" *)

  (* added productions *)

command_entry: [
| noedit_mode
]

tactic_expr1: [
| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
| MOVETO ltac_match_goal match_key OPT "reverse" "goal" "with" match_context_list "end"
| MOVETO ltac_match_term match_key tactic_expr5 "with" match_list "end"
| REPLACE failkw [ int_or_var | ] LIST0 message_token
| WITH failkw OPT int_or_var LIST0 message_token
]

DELETE: [
| tactic_then_locality
]

tactic_expr4: [
| REPLACE tactic_expr3 ";" tactic_then_gen "]"
| WITH tactic_expr3 ";" "[" tactic_then_gen "]"
| tactic_expr3 ";" "[" ">" tactic_then_gen "]"
]

match_context_list: [
| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
]

match_hyps: [
| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern
| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern
| DELETE name ":=" match_pattern
]

match_list: [
| EDIT ADD_OPT "|" LIST1 match_rule SEP "|"
]

match_rule: [
| REPLACE match_pattern "=>" tactic_expr5
| WITH [ match_pattern | "_" ] "=>" tactic_expr5
| DELETE "_" "=>" tactic_expr5
]


selector_body: [
| REPLACE range_selector_or_nth  (* depends on whether range_selector_or_nth is deleted first *)
| WITH LIST1 range_selector SEP ","
]

range_selector_or_nth: [ | DELETENT ]

simple_tactic: [
| DELETE "intros"
| REPLACE "intros" ne_intropatterns
| WITH "intros" intropatterns
| DELETE "eintros"
| REPLACE "eintros" ne_intropatterns
| WITH "eintros" intropatterns
]

(* 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 [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
| WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string
| INSERTALL "Print"
]

command: [
| REPLACE "Print" printable
| WITH printable
| "SubClass" ident_decl def_body
| REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with"
| WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body )
| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with"      (* funind plugin *)
| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc )      (* funind plugin *)
| REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
| WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )      (* funind plugin *)

]

only_parsing: [
| OPTINREF
]

syntax: [
| REPLACE "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
| WITH    "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ]
| REPLACE "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ]   OPT [ ":" IDENT ]
| WITH    "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ]
| REPLACE "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
| WITH    "Reserved" "Infix" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
| REPLACE "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
| WITH    "Reserved" "Notation" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
]

numnotoption: [
| OPTINREF
]

binder_tactic: [
| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5
]

tactic_then_gen: [
| OPTINREF
]

record_binder_body: [
| REPLACE binders of_type_with_opt_coercion lconstr
| WITH binders of_type_with_opt_coercion
| REPLACE binders of_type_with_opt_coercion lconstr ":=" lconstr
| WITH binders of_type_with_opt_coercion ":=" lconstr
]

simple_assum_coe: [
| REPLACE LIST1 ident_decl of_type_with_opt_coercion lconstr
| WITH LIST1 ident_decl of_type_with_opt_coercion
]

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

(* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
(* consider tactic_command vs tac2mode *)
vernac_aux: [
| tactic_mode "."
]

def_token: [
| DELETE "SubClass" (* document separately from Definition and Example *)
]

assumption_token: [
| REPLACE "Axiom"
| WITH [ "Axiom" | "Axioms" ]
| REPLACE "Conjecture"
| WITH [ "Conjecture" | "Conjectures" ]
| REPLACE "Hypothesis"
| WITH [ "Hypothesis" | "Hypotheses" ]
| REPLACE "Parameter"
| WITH [ "Parameter" | "Parameters" ]
| REPLACE "Variable"
| WITH [ "Variable" | "Variables" ]
]

legacy_attrs: [
| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private"
]

all_attrs: [
| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs
]

vernacular: [
| LIST0 ( OPT all_attrs [ command | tactic ] "." )
]

rec_definition: [
| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
]

corec_definition: [
| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
]

type_cstr: [
| REPLACE ":" lconstr
| WITH ":" type
| OPTINREF
]

inductive_definition: [
| REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
| WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations
]

constructor_list_or_record_decl: [
| DELETE "|" LIST1 constructor SEP "|"
| REPLACE identref constructor_type "|" LIST1 constructor SEP "|"
| WITH OPT "|" LIST1 constructor SEP "|"
| DELETE identref constructor_type
| REPLACE identref "{" record_fields "}"
| WITH OPT identref "{" record_fields "}"
| DELETE "{" record_fields "}"
]

record_binder: [
| REPLACE name record_binder_body
| WITH name OPT record_binder_body
| DELETE name
]

in_clause: [
| DELETE in_clause'
| REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ
| WITH LIST0 hypident_occ SEP "," OPT ( "|-" concl_occ )
| DELETE LIST0 hypident_occ SEP ","
]

concl_occ: [
| OPTINREF
]

opt_coercion: [
| OPTINREF
]

opt_constructors_or_fields: [
| OPTINREF
]

decl_notations: [
| REPLACE "where" LIST1 decl_notation SEP decl_sep
| WITH "where" decl_notation LIST0 (decl_sep decl_notation )
| OPTINREF
]

SPLICE: [
| noedit_mode
| command_entry
| bigint
| match_list
| match_context_list
| IDENT
| LEFTQMARK
| natural
| NUMERAL
| STRING
| hyp
| var
| identref
| pattern_ident
| constr_eval  (* splices as multiple prods *)
| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
| Prim.name
| ltac_selector
| Constr.ident
| attribute_list
| operconstr99
| operconstr90
| operconstr9
| operconstr8
| pattern200
| pattern99
| pattern90
| ne_lstring
| ne_string
| lstring
| basequalid
| fullyqualid
| global
| reference
| bar_cbrace
| lconstr

(*
| ast_closure_term
| ast_closure_lterm
| ident_no_do
| ssrterm
| ssrtacarg
| ssrtac3arg
| ssrtclarg
| ssrhyp
| ssrhoi_hyp
| ssrhoi_id
| ssrindex
| ssrhpats
| ssrhpats_nobs
| ssrfwdid
| ssrmovearg
| ssrcasearg
| ssrrwargs
| ssrviewposspc
| ssrpatternarg
| ssr_elsepat
| ssr_mpat
| ssrunlockargs
| ssrcofixfwd
| ssrfixfwd
| ssrhavefwdwbinders
| ssripats_ne
| ssrparentacarg
| ssrposefwd
*)

| preident
| lpar_id_coloneq
| binders
| casted_constr
| check_module_types
| constr_pattern
| decl_sep
| function_rec_definition_loc (* loses funind annotation *)
| glob
| glob_constr_with_bindings
| id_or_meta
| lconstr_pattern
| lglob
| ltac_tacdef_body
| mode
| mult_pattern
| open_constr
| option_table
| record_declaration
| register_type_token
| tactic
| uconstr
| impl_ident_head
| branches
| check_module_type
| decorated_vernac
| ext_module_expr
| ext_module_type
| pattern_identref
| test
| binder_constr
| atomic_constr
| let_type_cstr
| name_colon
| closed_binder
| binders_fixannot
| as_return_type
| case_type
| fields_def
| universe_increment
| type_cstr
| record_pattern
| evar_instance
| fix_decls
| cofix_decls
| assum_list
| assum_coe
| inline
| occs
| univ_name_list
| ltac_info
| field_mods
| ltac_production_sep
| ltac_tactic_level
| printunivs_subgraph
| ring_mods
| scope_delimiter
| eliminator  (* todo: splice or not? *)
| quoted_attributes  (* todo: splice or not? *)
| printable
| only_parsing
| def_token
| record_fields
| constructor_type
| record_binder
| opt_coercion
| opt_constructors_or_fields
] (* end SPLICE *)

RENAME: [
| clause clause_dft_concl

| 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 *)
| tactic_expr5 ltac_expr
| tactic_expr4 ltac_expr4
| tactic_expr3 ltac_expr3
| tactic_expr2 ltac_expr2
| tactic_expr1 ltac_expr1
| tactic_expr0 ltac_expr0

(* | nonsimple_intropattern intropattern (* ltac2 *) *)
| intropatterns intropattern_list_opt

| operconstr200 term   (* historical name *)
| operconstr100 term100
| operconstr10 term10
| operconstr1 term1
| operconstr0 term0
| pattern100 pattern
| match_constr term_match
(*| impl_ident_tail impl_ident*)
| ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)

| tactic_then_gen multi_goal_tactics
| selector only_selector
| selector_body selector
| input_fun fun_var
| match_hyps match_hyp

| BULLET bullet
| nat_or_var num_or_var
| fix_decl fix_body
| cofix_decl cofix_body
| constr one_term
| appl_arg arg
| rec_definition fix_definition
| corec_definition cofix_definition
| inst evar_binding
| univ_instance univ_annot
| simple_assum_coe assumpt
| of_type_with_opt_coercion of_type
| attribute attr
| attribute_value attr_value
| constructor_list_or_record_decl constructors_or_record
| record_binder_body field_body
| class_rawexpr class
| smart_global smart_qualid
]


(* todo: ssrreflect*.rst ref to fix_body is incorrect *)