(* Defines the order to apply to editedGrammar to get productionlistGrammar.
doc_grammar will modify this file to add/remove nonterminals and productions
to match editedGrammar, which will remove comments.  Not compiled into Coq *)
DOC_GRAMMAR

vernac_toplevel: [
| "Drop" "."
| "Quit" "."
| "BackTo" num "."
| "Show" "Goal" num "at" num "."
| "Show" "Proof" "Diffs" OPT "removed" "."
| vernac_control
]

tactic_mode: [
| OPT toplevel_selector query_command
| OPT toplevel_selector "{"
| OPT toplevel_selector OPT ( "Info" num ) ltac_expr ltac_use_default
| "par" ":" OPT ( "Info" num ) ltac_expr ltac_use_default
]

ltac_use_default: [
| "."
| "..."
]

vernac_control: [
| "Time" vernac_control
| "Redirect" string vernac_control
| "Timeout" num vernac_control
| "Fail" vernac_control
| LIST0 ( "#[" LIST0 attr SEP "," "]" ) vernac
]

term: [
| "forall" open_binders "," term
| "fun" open_binders "=>" term
| term_let
| "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
| term_fix
| term_cofix
| term100
]

term100: [
| term_cast
| term10
]

term10: [
| term1 LIST1 arg
| "@" qualid OPT univ_annot LIST0 term1
| term1
]

arg: [
| "(" ident ":=" term ")"
| term1
]

one_term: [
| term1
| "@" qualid OPT univ_annot
]

term1: [
| term_projection
| term0 "%" ident
| term0
]

term0: [
| qualid OPT univ_annot
| sort
| numeral
| string
| "_"
| term_evar
| term_match
| "(" term ")"
| "{|" LIST0 field_def "|}"
| "`{" term "}"
| "`(" term ")"
| "ltac" ":" "(" ltac_expr ")"
]

field_def: [
| qualid LIST0 binder ":=" term
]

term_projection: [
| term0 ".(" qualid LIST0 arg ")"
| term0 ".(" "@" qualid LIST0 ( term1 ) ")"
]

term_evar: [
| "?[" ident "]"
| "?[" "?" ident "]"
| "?" ident OPT ( "@{" LIST1 evar_binding SEP ";" "}" )
]

evar_binding: [
| ident ":=" term
]

dangling_pattern_extension_rule: [
| "@" "?" ident LIST1 ident
]

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

assumpt: [
| LIST1 ident_decl of_type
]

ident_decl: [
| ident OPT univ_decl
]

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

qualid: [
| ident LIST0 field_ident
]

field_ident: [
| "." ident
]

type: [
| term
]

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

int: [
| OPT "-" LIST1 digit
]

num: [
| LIST1 digit
]

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

ident: [
| first_letter LIST0 subsequent_letter
]

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

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

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

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

attr: [
| ident OPT attr_value
]

attr_value: [
| "=" string
| "(" LIST0 attr SEP "," ")"
]

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

sort: [
| "Set"
| "Prop"
| "SProp"
| "Type"
| "Type" "@{" "_" "}"
| "Type" "@{" universe "}"
]

universe: [
| "max" "(" LIST1 universe_expr SEP "," ")"
| universe_expr
]

universe_expr: [
| universe_name OPT ( "+" num )
]

universe_name: [
| qualid
| "Set"
| "Prop"
]

univ_annot: [
| "@{" LIST0 universe_level "}"
]

universe_level: [
| "Set"
| "Prop"
| "Type"
| "_"
| qualid
]

univ_decl: [
| "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
]

univ_constraint: [
| universe_name [ "<" | "=" | "<=" ] universe_name
]

term_fix: [
| "let" "fix" fix_body "in" term
| "fix" fix_body OPT ( LIST1 ( "with" fix_body ) "for" ident )
]

fix_body: [
| ident LIST0 binder OPT fixannot OPT ( ":" type ) ":=" term
]

fixannot: [
| "{" "struct" ident "}"
| "{" "wf" one_term ident "}"
| "{" "measure" one_term OPT ident OPT one_term "}"
]

term_cofix: [
| "let" "cofix" cofix_body "in" term
| "cofix" cofix_body OPT ( LIST1 ( "with" cofix_body ) "for" ident )
]

cofix_body: [
| ident LIST0 binder OPT ( ":" type ) ":=" term
]

term_let: [
| "let" name OPT ( ":" type ) ":=" term "in" term
| "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
| "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term
| "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term
| "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term
]

open_binders: [
| LIST1 name ":" term
| LIST1 binder
]

name: [
| "_"
| ident
]

binder: [
| name
| "(" LIST1 name ":" type ")"
| "(" name OPT ( ":" type ) ":=" term ")"
| "(" name ":" type "|" term ")"
| "{" LIST1 name OPT ( ":" type ) "}"
| "[" LIST1 name OPT ( ":" type ) "]"
| "`(" LIST1 typeclass_constraint SEP "," ")"
| "`{" LIST1 typeclass_constraint SEP "," "}"
| "`[" LIST1 typeclass_constraint SEP "," "]"
| "'" pattern0
]

typeclass_constraint: [
| OPT "!" term
| "{" name "}" ":" OPT "!" term
| name ":" OPT "!" term
]

term_cast: [
| term10 "<:" term
| term10 "<<:" term
| term10 ":" term
| term10 ":>"
]

term_match: [
| "match" LIST1 case_item SEP "," OPT ( "return" term100 ) "with" OPT "|" LIST0 eqn SEP "|" "end"
]

case_item: [
| term100 OPT ( "as" name ) OPT [ "in" pattern ]
]

eqn: [
| LIST1 [ LIST1 pattern SEP "," ] SEP "|" "=>" term
]

pattern: [
| pattern10 ":" term
| pattern10
]

pattern10: [
| pattern1 "as" name
| pattern1 LIST0 pattern1
| "@" qualid LIST0 pattern1
]

pattern1: [
| pattern0 "%" ident
| pattern0
]

pattern0: [
| qualid
| "{|" LIST0 ( qualid ":=" pattern ) "|}"
| "_"
| "(" LIST1 pattern SEP "|" ")"
| numeral
| string
]

vernac: [
| "Local" vernac_poly
| "Global" vernac_poly
| vernac_poly
]

vernac_poly: [
| "Polymorphic" vernac_aux
| "Monomorphic" vernac_aux
| vernac_aux
]

vernac_aux: [
| "Program" gallina "."
| "Program" gallina_ext "."
| gallina "."
| gallina_ext "."
| command "."
| tactic_mode "."
| syntax "."
| subprf
| query_command
]

subprf: [
| bullet
| "{"
| "}"
]

gallina: [
| thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
| [ "Definition" | "Example" ] ident_decl def_body
| "Let" ident def_body
| "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 )
| "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition )
| "Scheme" scheme LIST0 ( "with" scheme )
| "Combined" "Scheme" ident "from" LIST1 ident SEP ","
| "Register" qualid "as" qualid
| "Register" "Inline" qualid
| "Primitive" ident OPT [ ":" term ] ":=" register_token
| "Universe" LIST1 ident
| "Universes" LIST1 ident
| "Constraint" LIST1 univ_constraint SEP ","
]

fix_definition: [
| ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
]

decl_notations: [
| "where" decl_notation LIST0 ( "and" decl_notation )
]

decl_notation: [
| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ]
]

register_token: [
| register_prim_token
| "#int63_type"
| "#float64_type"
]

register_prim_token: [
| "#int63_head0"
| "#int63_tail0"
| "#int63_add"
| "#int63_sub"
| "#int63_mul"
| "#int63_div"
| "#int63_mod"
| "#int63_lsr"
| "#int63_lsl"
| "#int63_land"
| "#int63_lor"
| "#int63_lxor"
| "#int63_addc"
| "#int63_subc"
| "#int63_addcarryc"
| "#int63_subcarryc"
| "#int63_mulc"
| "#int63_diveucl"
| "#int63_div21"
| "#int63_addmuldiv"
| "#int63_eq"
| "#int63_lt"
| "#int63_le"
| "#int63_compare"
| "#float64_opp"
| "#float64_abs"
| "#float64_eq"
| "#float64_lt"
| "#float64_le"
| "#float64_compare"
| "#float64_classify"
| "#float64_add"
| "#float64_sub"
| "#float64_mul"
| "#float64_div"
| "#float64_sqrt"
| "#float64_of_int63"
| "#float64_normfr_mantissa"
| "#float64_frshiftexp"
| "#float64_ldshiftexp"
| "#float64_next_up"
| "#float64_next_down"
]

thm_token: [
| "Theorem"
| "Lemma"
| "Fact"
| "Remark"
| "Corollary"
| "Proposition"
| "Property"
]

def_body: [
| LIST0 binder OPT ( ":" type ) ":=" OPT reduce term
| LIST0 binder ":" type
]

reduce: [
| "Eval" red_expr "in"
]

red_expr: [
| "red"
| "hnf"
| "simpl" OPT delta_flag OPT ref_or_pattern_occ
| "cbv" OPT strategy_flag
| "cbn" OPT strategy_flag
| "lazy" OPT strategy_flag
| "compute" OPT delta_flag
| "vm_compute" OPT ref_or_pattern_occ
| "native_compute" OPT ref_or_pattern_occ
| "unfold" LIST1 unfold_occ SEP ","
| "fold" LIST1 one_term
| "pattern" LIST1 pattern_occ SEP ","
| ident
]

delta_flag: [
| OPT "-" "[" LIST1 smart_qualid "]"
]

smart_qualid: [
| qualid
| by_notation
]

by_notation: [
| string OPT [ "%" ident ]
]

strategy_flag: [
| LIST1 red_flags
| delta_flag
]

red_flags: [
| "beta"
| "iota"
| "match"
| "fix"
| "cofix"
| "zeta"
| "delta" OPT delta_flag
]

ref_or_pattern_occ: [
| smart_qualid OPT ( "at" occs_nums )
| one_term OPT ( "at" occs_nums )
]

occs_nums: [
| LIST1 num_or_var
| "-" num_or_var LIST0 int_or_var
]

num_or_var: [
| num
| ident
]

int_or_var: [
| int
| ident
]

unfold_occ: [
| smart_qualid OPT ( "at" occs_nums )
]

pattern_occ: [
| one_term OPT ( "at" occs_nums )
]

finite_token: [
| "Inductive"
| "CoInductive"
| "Variant"
| "Record"
| "Structure"
| "Class"
]

inductive_definition: [
| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
]

constructors_or_record: [
| OPT "|" LIST1 constructor SEP "|"
| OPT ident "{" LIST1 record_field SEP ";" "}"
]

constructor: [
| ident LIST0 binder OPT of_type
]

record_field: [
| LIST0 ( "#[" LIST0 attr SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
]

field_body: [
| LIST0 binder of_type
| LIST0 binder of_type ":=" term
| LIST0 binder ":=" term
]

cofix_definition: [
| ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
]

scheme: [
| scheme_kind
| ident ":=" scheme_kind
]

scheme_kind: [
| "Induction" "for" smart_qualid "Sort" sort_family
| "Minimality" "for" smart_qualid "Sort" sort_family
| "Elimination" "for" smart_qualid "Sort" sort_family
| "Case" "for" smart_qualid "Sort" sort_family
| "Equality" "for" smart_qualid
]

sort_family: [
| "Set"
| "Prop"
| "SProp"
| "Type"
]

gallina_ext: [
| "Module" OPT export_token ident LIST0 module_binder of_module_type OPT is_module_expr
| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT is_module_type
| "Declare" "Module" OPT export_token ident LIST0 module_binder ":" module_type_inl
| "Section" ident
| "Chapter" ident
| "End" ident
| "Collection" ident ":=" section_subset_expr
| "Require" OPT export_token LIST1 qualid
| "From" qualid "Require" OPT export_token LIST1 qualid
| "Import" LIST1 qualid
| "Export" LIST1 qualid
| "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
| "Include" "Type" module_type_inl LIST0 ( "<+" module_type_inl )
| "Transparent" LIST1 smart_qualid
| "Opaque" LIST1 smart_qualid
| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ]
| "Canonical" OPT "Structure" qualid OPT [ OPT univ_decl def_body ]
| "Canonical" OPT "Structure" by_notation
| "Coercion" qualid OPT univ_decl def_body
| "Identity" "Coercion" ident ":" class ">->" class
| "Coercion" qualid ":" class ">->" class
| "Coercion" by_notation ":" class ">->" class
| "Context" LIST1 binder
| "Instance" instance_name ":" term hint_info [ ":=" "{" [ LIST1 field_def SEP ";" | ] "}" | ":=" term | ]
| "Existing" "Instance" qualid hint_info
| "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
| "Existing" "Class" qualid
| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
| "Implicit" "Type" reserv_list
| "Implicit" "Types" reserv_list
| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ]
| "Export" "Set" LIST1 ident option_setting
| "Export" "Unset" LIST1 ident
]

option_setting: [
|
| int
| string
]

hint_info: [
| "|" OPT num OPT one_term
|
]

export_token: [
| "Import"
| "Export"
]

module_binder: [
| "(" OPT export_token LIST1 ident ":" module_type_inl ")"
]

module_type_inl: [
| "!" module_type
| module_type OPT functor_app_annot
]

module_type: [
| qualid
| "(" module_type ")"
| module_type module_expr_atom
| module_type "with" with_declaration
]

with_declaration: [
| "Definition" qualid OPT univ_decl ":=" term
| "Module" qualid ":=" qualid
]

functor_app_annot: [
| "[" "inline" "at" "level" num "]"
| "[" "no" "inline" "]"
]

of_module_type: [
| ":" module_type_inl
| LIST0 ( "<:" module_type_inl )
]

is_module_type: [
| ":=" module_type_inl LIST0 ( "<+" module_type_inl )
]

module_expr_atom: [
| qualid
| "(" module_expr ")"
]

module_expr: [
| module_expr_atom
| module_expr module_expr_atom
]

is_module_expr: [
| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl )
]

module_expr_inl: [
| "!" module_expr
| module_expr OPT functor_app_annot
]

argument_spec_block: [
| argument_spec
| "/"
| "&"
| "(" LIST1 argument_spec ")" OPT ( "%" ident )
| "[" LIST1 argument_spec "]" OPT ( "%" ident )
| "{" LIST1 argument_spec "}" OPT ( "%" ident )
]

argument_spec: [
| OPT "!" name OPT ( "%" ident )
]

more_implicits_block: [
| name
| "[" LIST1 name "]"
| "{" LIST1 name "}"
]

arguments_modifier: [
| "simpl" "nomatch"
| "simpl" "never"
| "default" "implicits"
| "clear" "bidirectionality" "hint"
| "clear" "implicits"
| "clear" "scopes"
| "clear" "scopes" "and" "implicits"
| "clear" "implicits" "and" "scopes"
| "rename"
| "assert"
| "extra" "scopes"
]

strategy_level: [
| "expand"
| "opaque"
| int
| "transparent"
]

instance_name: [
| ident_decl LIST0 binder
|
]

reserv_list: [
| LIST1 reserv_tuple
| simple_reserv
]

reserv_tuple: [
| "(" simple_reserv ")"
]

simple_reserv: [
| LIST1 ident ":" term
]

command: [
| "Goal" term
| "Declare" "Scope" ident
| "Pwd"
| "Cd"
| "Cd" string
| "Load" [ "Verbose" | ] [ string | ident ]
| "Declare" "ML" "Module" LIST1 string
| "Locate" locatable
| "Add" "LoadPath" string "as" dirpath
| "Add" "Rec" "LoadPath" string "as" dirpath
| "Remove" "LoadPath" string
| "Type" term
| "Print" "Term" smart_qualid OPT ( "@{" LIST0 name "}" )
| "Print" "All"
| "Print" "Section" qualid
| "Print" "Grammar" ident
| "Print" "Custom" "Grammar" ident
| "Print" "LoadPath" OPT dirpath
| "Print" "Modules"
| "Print" "Libraries"
| "Print" "ML" "Path"
| "Print" "ML" "Modules"
| "Print" "Debug" "GC"
| "Print" "Graph"
| "Print" "Classes"
| "Print" "TypeClasses"
| "Print" "Instances" smart_qualid
| "Print" "Coercions"
| "Print" "Coercion" "Paths" class class
| "Print" "Canonical" "Projections" LIST0 smart_qualid
| "Print" "Typing" "Flags"
| "Print" "Tables"
| "Print" "Options"
| "Print" "Hint"
| "Print" "Hint" smart_qualid
| "Print" "Hint" "*"
| "Print" "HintDb" ident
| "Print" "Scopes"
| "Print" "Scope" ident
| "Print" "Visibility" OPT ident
| "Print" "Implicit" smart_qualid
| "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
| "Print" "Assumptions" smart_qualid
| "Print" "Opaque" "Dependencies" smart_qualid
| "Print" "Transparent" "Dependencies" smart_qualid
| "Print" "All" "Dependencies" smart_qualid
| "Print" "Strategy" smart_qualid
| "Print" "Strategies"
| "Print" "Registered"
| "Print" smart_qualid OPT ( "@{" LIST0 name "}" )
| "Print" "Module" "Type" qualid
| "Print" "Module" qualid
| "Print" "Namespace" dirpath
| "Inspect" num
| "Add" "ML" "Path" string
| "Set" LIST1 ident option_setting
| "Unset" LIST1 ident
| "Print" "Table" LIST1 ident
| "Add" ident ident LIST1 option_ref_value
| "Add" ident LIST1 option_ref_value
| "Test" LIST1 ident "for" LIST1 option_ref_value
| "Test" LIST1 ident
| "Remove" ident ident LIST1 option_ref_value
| "Remove" ident LIST1 option_ref_value
| "Write" "State" ident
| "Write" "State" string
| "Restore" "State" ident
| "Restore" "State" string
| "Reset" "Initial"
| "Reset" ident
| "Back"
| "Back" num
| "Debug" "On"
| "Debug" "Off"
| "Declare" "Reduction" ident ":=" red_expr
| "Declare" "Custom" "Entry" ident
| "Derive" ident "SuchThat" one_term "As" ident      (* derive plugin *)
| "Proof"
| "Proof" "Mode" string
| "Proof" term
| "Abort"
| "Abort" "All"
| "Abort" ident
| "Existential" num constr_body
| "Admitted"
| "Qed"
| "Save" ident
| "Defined"
| "Defined" ident
| "Restart"
| "Undo"
| "Undo" num
| "Undo" "To" num
| "Focus"
| "Focus" num
| "Unfocus"
| "Unfocused"
| "Show"
| "Show" num
| "Show" ident
| "Show" "Existentials"
| "Show" "Universes"
| "Show" "Conjectures"
| "Show" "Proof"
| "Show" "Intro"
| "Show" "Intros"
| "Show" "Match" qualid
| "Guarded"
| "Create" "HintDb" ident [ "discriminated" | ]
| "Remove" "Hints" LIST1 qualid opt_hintbases
| "Hint" hint opt_hintbases
| "Comments" LIST0 comment
| "Declare" "Instance" ident_decl LIST0 binder ":" term hint_info
| "Obligation" int "of" ident ":" term withtac
| "Obligation" int "of" ident withtac
| "Obligation" int ":" term withtac
| "Obligation" int withtac
| "Next" "Obligation" "of" ident withtac
| "Next" "Obligation" withtac
| "Solve" "Obligation" int "of" ident "with" ltac_expr
| "Solve" "Obligation" int "with" ltac_expr
| "Solve" "Obligations" "of" ident "with" ltac_expr
| "Solve" "Obligations" "with" ltac_expr
| "Solve" "Obligations"
| "Solve" "All" "Obligations" "with" ltac_expr
| "Solve" "All" "Obligations"
| "Admit" "Obligations" "of" ident
| "Admit" "Obligations"
| "Obligation" "Tactic" ":=" ltac_expr
| "Show" "Obligation" "Tactic"
| "Obligations" "of" ident
| "Obligations"
| "Preterm" "of" ident
| "Preterm"
| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident
| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "as" ident
| "Add" "Relation" one_term one_term "as" ident
| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "as" ident
| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
| "Add" "Relation" one_term one_term "transitivity" "proved" "by" one_term "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "transitivity" "proved" "by" one_term "as" ident
| "Add" "Setoid" one_term one_term one_term "as" ident
| "Add" "Parametric" "Setoid" LIST0 binder ":" one_term one_term one_term "as" ident
| "Add" "Morphism" one_term ":" ident
| "Declare" "Morphism" one_term ":" ident
| "Add" "Morphism" one_term "with" "signature" term "as" ident
| "Add" "Parametric" "Morphism" LIST0 binder ":" one_term "with" "signature" term "as" ident
| "Grab" "Existential" "Variables"
| "Unshelve"
| "Declare" "Equivalent" "Keys" one_term one_term
| "Print" "Equivalent" "Keys"
| "Optimize" "Proof"
| "Optimize" "Heap"
| "Reset" "Ltac" "Profile"
| "Show" "Ltac" "Profile"
| "Show" "Ltac" "Profile" "CutOff" int
| "Show" "Ltac" "Profile" string
| "Show" "Lia" "Profile"      (* micromega plugin *)
| "Add" "InjTyp" one_term      (* micromega plugin *)
| "Add" "BinOp" one_term      (* micromega plugin *)
| "Add" "UnOp" one_term      (* micromega plugin *)
| "Add" "CstOp" one_term      (* micromega plugin *)
| "Add" "BinRel" one_term      (* micromega plugin *)
| "Add" "PropOp" one_term      (* micromega plugin *)
| "Add" "PropBinOp" one_term      (* micromega plugin *)
| "Add" "PropUOp" one_term      (* micromega plugin *)
| "Add" "Spec" one_term      (* micromega plugin *)
| "Add" "BinOpSpec" one_term      (* micromega plugin *)
| "Add" "UnOpSpec" one_term      (* micromega plugin *)
| "Add" "Saturate" one_term      (* micromega plugin *)
| "Show" "Zify" "InjTyp"      (* micromega plugin *)
| "Show" "Zify" "BinOp"      (* micromega plugin *)
| "Show" "Zify" "UnOp"      (* micromega plugin *)
| "Show" "Zify" "CstOp"      (* micromega plugin *)
| "Show" "Zify" "BinRel"      (* micromega plugin *)
| "Show" "Zify" "Spec"      (* micromega plugin *)
| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* setoid_ring plugin *)
| "Hint" "Cut" "[" hints_path "]" opthints
| "Typeclasses" "Transparent" LIST0 qualid
| "Typeclasses" "Opaque" LIST0 qualid
| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int
| "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
| "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
| "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
| "Print" "Rewrite" "HintDb" ident
| "Print" "Ltac" qualid
| "Locate" "Ltac" qualid
| "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
| "Print" "Ltac" "Signatures"
| "Set" "Firstorder" "Solver" ltac_expr
| "Print" "Firstorder" "Solver"
| "Function" fix_definition LIST0 ( "with" fix_definition )
| "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg )
| "Extraction" qualid      (* extraction plugin *)
| "Recursive" "Extraction" LIST1 qualid      (* extraction plugin *)
| "Extraction" string LIST1 qualid      (* extraction plugin *)
| "Extraction" "TestCompile" LIST1 qualid      (* extraction plugin *)
| "Separate" "Extraction" LIST1 qualid      (* extraction plugin *)
| "Extraction" "Library" ident      (* extraction plugin *)
| "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
| "Extraction" "Language" language      (* extraction plugin *)
| "Extraction" "Inline" LIST1 qualid      (* extraction plugin *)
| "Extraction" "NoInline" LIST1 qualid      (* extraction plugin *)
| "Print" "Extraction" "Inline"      (* extraction plugin *)
| "Reset" "Extraction" "Inline"      (* extraction plugin *)
| "Extraction" "Implicit" qualid "[" LIST0 int_or_id "]"      (* extraction plugin *)
| "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
| "Extract" "Constant" qualid LIST0 string "=>" mlname      (* extraction plugin *)
| "Extract" "Inlined" "Constant" qualid "=>" mlname      (* extraction plugin *)
| "Extract" "Inductive" qualid "=>" mlname "[" LIST0 mlname "]" OPT string      (* extraction plugin *)
| "Show" "Extraction"      (* extraction plugin *)
| "Functional" "Case" fun_scheme_arg      (* funind plugin *)
| "Generate" "graph" "for" qualid      (* funind plugin *)
| "Hint" "Rewrite" orient LIST1 one_term ":" LIST0 ident
| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr ":" LIST0 ident
| "Hint" "Rewrite" orient LIST1 one_term
| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr
| "Derive" "Inversion_clear" ident "with" one_term "Sort" sort_family
| "Derive" "Inversion_clear" ident "with" one_term
| "Derive" "Inversion" ident "with" one_term "Sort" sort_family
| "Derive" "Inversion" ident "with" one_term
| "Derive" "Dependent" "Inversion" ident "with" one_term "Sort" sort_family
| "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
| "Declare" "Left" "Step" one_term
| "Declare" "Right" "Step" one_term
| "Print" "Rings"      (* setoid_ring plugin *)
| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
| "Print" "Fields"      (* setoid_ring plugin *)
| "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption
| "String" "Notation" qualid qualid qualid ":" ident
| "SubClass" ident_decl def_body
]

orient: [
| "->"
| "<-"
|
]

section_subset_expr: [
| LIST0 starredidentref
| ssexpr
]

ssexpr: [
| "-" ssexpr50
| ssexpr50
]

ssexpr50: [
| ssexpr0 "-" ssexpr0
| ssexpr0 "+" ssexpr0
| ssexpr0
]

ssexpr0: [
| starredidentref
| "(" LIST0 starredidentref ")"
| "(" LIST0 starredidentref ")" "*"
| "(" ssexpr ")"
| "(" ssexpr ")" "*"
]

starredidentref: [
| ident
| ident "*"
| "Type"
| "Type" "*"
]

dirpath: [
| ident
| dirpath field_ident
]

locatable: [
| smart_qualid
| "Term" smart_qualid
| "File" string
| "Library" qualid
| "Module" qualid
]

option_ref_value: [
| qualid
| string
]

comment: [
| one_term
| string
| num
]

reference_or_constr: [
| qualid
| one_term
]

hint: [
| "Resolve" LIST1 reference_or_constr hint_info
| "Resolve" "->" LIST1 qualid OPT num
| "Resolve" "<-" LIST1 qualid OPT num
| "Immediate" LIST1 reference_or_constr
| "Variables" "Transparent"
| "Variables" "Opaque"
| "Constants" "Transparent"
| "Constants" "Opaque"
| "Transparent" LIST1 qualid
| "Opaque" LIST1 qualid
| "Mode" qualid LIST1 [ "+" | "!" | "-" ]
| "Unfold" LIST1 qualid
| "Constructors" LIST1 qualid
| "Extern" num OPT one_term "=>" ltac_expr
]

constr_body: [
| ":=" term
| ":" term ":=" term
]

withtac: [
| "with" ltac_expr
|
]

ltac_def_kind: [
| ":="
| "::="
]

tacdef_body: [
| qualid LIST1 fun_var ltac_def_kind ltac_expr
| qualid ltac_def_kind ltac_expr
]

ltac_production_item: [
| string
| ident "(" ident OPT ( "," string ) ")"
| ident
]

numnotoption: [
| "(" "warning" "after" num ")"
| "(" "abstract" "after" num ")"
]

mlname: [
| ident      (* extraction plugin *)
| string      (* extraction plugin *)
]

int_or_id: [
| ident      (* extraction plugin *)
| int      (* extraction plugin *)
]

language: [
| "Ocaml"      (* extraction plugin *)
| "OCaml"      (* extraction plugin *)
| "Haskell"      (* extraction plugin *)
| "Scheme"      (* extraction plugin *)
| "JSON"      (* extraction plugin *)
]

fun_scheme_arg: [
| ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
]

ring_mod: [
| "decidable" one_term      (* setoid_ring plugin *)
| "abstract"      (* setoid_ring plugin *)
| "morphism" one_term      (* setoid_ring plugin *)
| "constants" "[" ltac_expr "]"      (* setoid_ring plugin *)
| "preprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
| "postprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
| "setoid" one_term one_term      (* setoid_ring plugin *)
| "sign" one_term      (* setoid_ring plugin *)
| "power" one_term "[" LIST1 qualid "]"      (* setoid_ring plugin *)
| "power_tac" one_term "[" ltac_expr "]"      (* setoid_ring plugin *)
| "div" one_term      (* setoid_ring plugin *)
| "closed" "[" LIST1 qualid "]"      (* setoid_ring plugin *)
]

field_mod: [
| ring_mod      (* setoid_ring plugin *)
| "completeness" one_term      (* setoid_ring plugin *)
]

debug: [
| "debug"
|
]

eauto_search_strategy: [
| "(bfs)"
| "(dfs)"
|
]

hints_path_atom: [
| LIST1 qualid
| "_"
]

hints_path: [
| "(" hints_path ")"
| hints_path "*"
| "emp"
| "eps"
| hints_path "|" hints_path
| hints_path_atom
| hints_path hints_path
]

opthints: [
| ":" LIST1 ident
|
]

opt_hintbases: [
|
| ":" LIST1 ident
]

query_command: [
| "Eval" red_expr "in" term "."
| "Compute" term "."
| "Check" term "."
| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) "."
| "SearchHead" one_term in_or_out_modules "."
| "SearchPattern" one_term in_or_out_modules "."
| "SearchRewrite" one_term in_or_out_modules "."
| "Search" searchabout_query searchabout_queries "."
| "SearchAbout" searchabout_query searchabout_queries "."
| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
]

class: [
| "Funclass"
| "Sortclass"
| smart_qualid
]

ne_in_or_out_modules: [
| "inside" LIST1 qualid
| "outside" LIST1 qualid
]

in_or_out_modules: [
| ne_in_or_out_modules
|
]

positive_search_mark: [
| "-"
|
]

searchabout_query: [
| positive_search_mark string OPT ( "%" ident )
| positive_search_mark one_term
]

searchabout_queries: [
| ne_in_or_out_modules
| searchabout_query searchabout_queries
|
]

syntax: [
| "Open" "Scope" ident
| "Close" "Scope" ident
| "Delimit" "Scope" ident "with" ident
| "Undelimit" "Scope" ident
| "Bind" "Scope" ident "with" LIST1 class
| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ]
| "Format" "Notation" string string string
| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
]

level: [
| "level" num
| "next" "level"
]

syntax_modifier: [
| "at" "level" num
| "in" "custom" ident
| "in" "custom" ident "at" "level" num
| "left" "associativity"
| "right" "associativity"
| "no" "associativity"
| "only" "printing"
| "only" "parsing"
| "format" string OPT string
| ident "," LIST1 ident SEP "," "at" level
| ident "at" level OPT constr_as_binder_kind
| ident constr_as_binder_kind
| ident syntax_extension_type
]

constr_as_binder_kind: [
| "as" "ident"
| "as" "pattern"
| "as" "strict" "pattern"
]

syntax_extension_type: [
| "ident"
| "global"
| "bigint"
| "binder"
| "constr"
| "constr" at_level_opt OPT constr_as_binder_kind
| "pattern"
| "pattern" "at" "level" num
| "strict" "pattern"
| "strict" "pattern" "at" "level" num
| "closed" "binder"
| "custom" ident at_level_opt OPT constr_as_binder_kind
]

at_level_opt: [
| "at" level
|
]

simple_tactic: [
| "reflexivity"
| "exact" one_term
| "assumption"
| "etransitivity"
| "cut" one_term
| "exact_no_check" one_term
| "vm_cast_no_check" one_term
| "native_cast_no_check" one_term
| "casetype" one_term
| "elimtype" one_term
| "lapply" one_term
| "transitivity" one_term
| "left"
| "eleft"
| "left" "with" bindings
| "eleft" "with" bindings
| "right"
| "eright"
| "right" "with" bindings
| "eright" "with" bindings
| "constructor"
| "constructor" int_or_var
| "constructor" int_or_var "with" bindings
| "econstructor"
| "econstructor" int_or_var
| "econstructor" int_or_var "with" bindings
| "specialize" constr_with_bindings
| "specialize" constr_with_bindings "as" simple_intropattern
| "symmetry"
| "symmetry" "in" in_clause
| "split"
| "esplit"
| "split" "with" bindings
| "esplit" "with" bindings
| "exists"
| "exists" LIST1 bindings SEP ","
| "eexists"
| "eexists" LIST1 bindings SEP ","
| "intros" "until" quantified_hypothesis
| "intro"
| "intro" ident
| "intro" ident "at" "top"
| "intro" ident "at" "bottom"
| "intro" ident "after" ident
| "intro" ident "before" ident
| "intro" "at" "top"
| "intro" "at" "bottom"
| "intro" "after" ident
| "intro" "before" ident
| "move" ident "at" "top"
| "move" ident "at" "bottom"
| "move" ident "after" ident
| "move" ident "before" ident
| "rename" LIST1 rename SEP ","
| "revert" LIST1 ident
| "simple" "induction" quantified_hypothesis
| "simple" "destruct" quantified_hypothesis
| "double" "induction" quantified_hypothesis quantified_hypothesis
| "admit"
| "fix" ident num
| "cofix" ident
| "clear" LIST0 ident
| "clear" "-" LIST1 ident
| "clearbody" LIST1 ident
| "generalize" "dependent" one_term
| "replace" one_term "with" one_term clause_dft_concl by_arg_tac
| "replace" "->" one_term clause_dft_concl
| "replace" "<-" one_term clause_dft_concl
| "replace" one_term clause_dft_concl
| "simplify_eq"
| "simplify_eq" destruction_arg
| "esimplify_eq"
| "esimplify_eq" destruction_arg
| "discriminate"
| "discriminate" destruction_arg
| "ediscriminate"
| "ediscriminate" destruction_arg
| "injection"
| "injection" destruction_arg
| "einjection"
| "einjection" destruction_arg
| "injection" "as" LIST0 simple_intropattern
| "injection" destruction_arg "as" LIST0 simple_intropattern
| "einjection" "as" LIST0 simple_intropattern
| "einjection" destruction_arg "as" LIST0 simple_intropattern
| "simple" "injection"
| "simple" "injection" destruction_arg
| "dependent" "rewrite" orient one_term
| "dependent" "rewrite" orient one_term "in" ident
| "cutrewrite" orient one_term
| "cutrewrite" orient one_term "in" ident
| "decompose" "sum" one_term
| "decompose" "record" one_term
| "absurd" one_term
| "contradiction" OPT constr_with_bindings
| "autorewrite" "with" LIST1 ident clause_dft_concl
| "autorewrite" "with" LIST1 ident clause_dft_concl "using" ltac_expr
| "autorewrite" "*" "with" LIST1 ident clause_dft_concl
| "autorewrite" "*" "with" LIST1 ident clause_dft_concl "using" ltac_expr
| "rewrite" "*" orient one_term "in" ident "at" occurrences by_arg_tac
| "rewrite" "*" orient one_term "at" occurrences "in" ident by_arg_tac
| "rewrite" "*" orient one_term "in" ident by_arg_tac
| "rewrite" "*" orient one_term "at" occurrences by_arg_tac
| "rewrite" "*" orient one_term by_arg_tac
| "refine" one_term
| "simple" "refine" one_term
| "notypeclasses" "refine" one_term
| "simple" "notypeclasses" "refine" one_term
| "solve_constraints"
| "subst" LIST1 ident
| "subst"
| "simple" "subst"
| "evar" "(" ident ":" term ")"
| "evar" one_term
| "instantiate" "(" ident ":=" term ")"
| "instantiate" "(" int ":=" term ")" hloc
| "instantiate"
| "stepl" one_term "by" ltac_expr
| "stepl" one_term
| "stepr" one_term "by" ltac_expr
| "stepr" one_term
| "generalize_eqs" ident
| "dependent" "generalize_eqs" ident
| "generalize_eqs_vars" ident
| "dependent" "generalize_eqs_vars" ident
| "specialize_eqs" ident
| "hresolve_core" "(" ident ":=" one_term ")" "at" int_or_var "in" one_term
| "hresolve_core" "(" ident ":=" one_term ")" "in" one_term
| "hget_evar" int_or_var
| "destauto"
| "destauto" "in" ident
| "transparent_abstract" ltac_expr3
| "transparent_abstract" ltac_expr3 "using" ident
| "constr_eq" one_term one_term
| "constr_eq_strict" one_term one_term
| "constr_eq_nounivs" one_term one_term
| "is_evar" one_term
| "has_evar" one_term
| "is_var" one_term
| "is_fix" one_term
| "is_cofix" one_term
| "is_ind" one_term
| "is_constructor" one_term
| "is_proj" one_term
| "is_const" one_term
| "shelve"
| "shelve_unifiable"
| "unshelve" ltac_expr1
| "give_up"
| "cycle" int_or_var
| "swap" int_or_var int_or_var
| "revgoals"
| "guard" int_or_var comparison int_or_var
| "decompose" "[" LIST1 one_term "]" one_term
| "optimize_heap"
| "start" "ltac" "profiling"
| "stop" "ltac" "profiling"
| "reset" "ltac" "profile"
| "show" "ltac" "profile"
| "show" "ltac" "profile" "cutoff" int
| "show" "ltac" "profile" string
| "restart_timer" OPT string
| "finish_timing" OPT string
| "finish_timing" "(" string ")" OPT string
| "eassumption"
| "eexact" one_term
| "trivial" auto_using hintbases
| "info_trivial" auto_using hintbases
| "debug" "trivial" auto_using hintbases
| "auto" OPT int_or_var auto_using hintbases
| "info_auto" OPT int_or_var auto_using hintbases
| "debug" "auto" OPT int_or_var auto_using hintbases
| "prolog" "[" LIST0 one_term "]" int_or_var
| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
| "new" "auto" OPT int_or_var auto_using hintbases
| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases
| "dfs" "eauto" OPT int_or_var auto_using hintbases
| "autounfold" hintbases clause_dft_concl
| "autounfold_one" hintbases "in" ident
| "autounfold_one" hintbases
| "unify" one_term one_term
| "unify" one_term one_term "with" ident
| "convert_concl_no_check" one_term
| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 ident
| "typeclasses" "eauto" OPT int_or_var "with" LIST1 ident
| "typeclasses" "eauto" OPT int_or_var
| "head_of_constr" ident one_term
| "not_evar" one_term
| "is_ground" one_term
| "autoapply" one_term "using" ident
| "autoapply" one_term "with" ident
| "progress_evars" ltac_expr
| "rewrite_strat" rewstrategy
| "rewrite_db" ident "in" ident
| "rewrite_db" ident
| "substitute" orient constr_with_bindings
| "setoid_rewrite" orient constr_with_bindings
| "setoid_rewrite" orient constr_with_bindings "in" ident
| "setoid_rewrite" orient constr_with_bindings "at" occurrences
| "setoid_rewrite" orient constr_with_bindings "at" occurrences "in" ident
| "setoid_rewrite" orient constr_with_bindings "in" ident "at" occurrences
| "setoid_symmetry"
| "setoid_symmetry" "in" ident
| "setoid_reflexivity"
| "setoid_transitivity" one_term
| "setoid_etransitivity"
| "decide" "equality"
| "compare" one_term one_term
| "rewrite_strat" rewstrategy "in" ident
| "intros" intropattern_list_opt
| "eintros" intropattern_list_opt
| "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
| "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
| "elim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
| "eelim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
| "case" induction_clause_list
| "ecase" induction_clause_list
| "fix" ident num "with" LIST1 fixdecl
| "cofix" ident "with" LIST1 cofixdecl
| "pose" bindings_with_parameters
| "pose" one_term as_name
| "epose" bindings_with_parameters
| "epose" one_term as_name
| "set" bindings_with_parameters clause_dft_concl
| "set" one_term as_name clause_dft_concl
| "eset" bindings_with_parameters clause_dft_concl
| "eset" one_term as_name clause_dft_concl
| "remember" one_term as_name eqn_ipat clause_dft_all
| "eremember" one_term as_name eqn_ipat clause_dft_all
| "assert" "(" ident ":=" term ")"
| "eassert" "(" ident ":=" term ")"
| "assert" "(" ident ":" term ")" by_tactic
| "eassert" "(" ident ":" term ")" by_tactic
| "enough" "(" ident ":" term ")" by_tactic
| "eenough" "(" ident ":" term ")" by_tactic
| "assert" one_term as_ipat by_tactic
| "eassert" one_term as_ipat by_tactic
| "pose" "proof" "(" ident ":=" term ")"
| "epose" "proof" "(" ident ":=" term ")"
| "pose" "proof" term as_ipat
| "epose" "proof" term as_ipat
| "enough" one_term as_ipat by_tactic
| "eenough" one_term as_ipat by_tactic
| "generalize" one_term
| "generalize" one_term LIST1 one_term
| "generalize" one_term OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ]
| "induction" induction_clause_list
| "einduction" induction_clause_list
| "destruct" induction_clause_list
| "edestruct" induction_clause_list
| "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
| "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" one_term ]
| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list
| "inversion" quantified_hypothesis "using" one_term in_hyp_list
| "red" clause_dft_concl
| "hnf" clause_dft_concl
| "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
| "cbv" OPT strategy_flag clause_dft_concl
| "cbn" OPT strategy_flag clause_dft_concl
| "lazy" OPT strategy_flag clause_dft_concl
| "compute" OPT delta_flag clause_dft_concl
| "vm_compute" OPT ref_or_pattern_occ clause_dft_concl
| "native_compute" OPT ref_or_pattern_occ clause_dft_concl
| "unfold" LIST1 unfold_occ SEP "," clause_dft_concl
| "fold" LIST1 one_term clause_dft_concl
| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl
| "change" conversion clause_dft_concl
| "change_no_check" conversion clause_dft_concl
| "btauto"
| "rtauto"
| "congruence"
| "congruence" int
| "congruence" "with" LIST1 one_term
| "congruence" int "with" LIST1 one_term
| "f_equal"
| "firstorder" OPT ltac_expr firstorder_using
| "firstorder" OPT ltac_expr "with" LIST1 ident
| "firstorder" OPT ltac_expr firstorder_using "with" LIST1 ident
| "gintuition" OPT ltac_expr
| "functional" "inversion" quantified_hypothesis OPT qualid      (* funind plugin *)
| "functional" "induction" LIST1 one_term fun_ind_using with_names      (* funind plugin *)
| "soft" "functional" "induction" LIST1 one_term fun_ind_using with_names      (* funind plugin *)
| "psatz_Z" int_or_var ltac_expr      (* micromega plugin *)
| "psatz_Z" ltac_expr      (* micromega plugin *)
| "xlia" ltac_expr      (* micromega plugin *)
| "xnlia" ltac_expr      (* micromega plugin *)
| "xnra" ltac_expr      (* micromega plugin *)
| "xnqa" ltac_expr      (* micromega plugin *)
| "sos_Z" ltac_expr      (* micromega plugin *)
| "sos_Q" ltac_expr      (* micromega plugin *)
| "sos_R" ltac_expr      (* micromega plugin *)
| "lra_Q" ltac_expr      (* micromega plugin *)
| "lra_R" ltac_expr      (* micromega plugin *)
| "psatz_R" int_or_var ltac_expr      (* micromega plugin *)
| "psatz_R" ltac_expr      (* micromega plugin *)
| "psatz_Q" int_or_var ltac_expr      (* micromega plugin *)
| "psatz_Q" ltac_expr      (* micromega plugin *)
| "zify_iter_specs"      (* micromega plugin *)
| "zify_op"      (* micromega plugin *)
| "zify_saturate"      (* micromega plugin *)
| "zify_iter_let" ltac_expr      (* micromega plugin *)
| "zify_elim_let"      (* micromega plugin *)
| "nsatz_compute" one_term      (* nsatz plugin *)
| "omega"      (* omega plugin *)
| "protect_fv" string "in" ident      (* setoid_ring plugin *)
| "protect_fv" string      (* setoid_ring plugin *)
| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* setoid_ring plugin *)
]

hloc: [
|
| "in" "|-" "*"
| "in" ident
| "in" "(" "Type" "of" ident ")"
| "in" "(" "Value" "of" ident ")"
| "in" "(" "type" "of" ident ")"
| "in" "(" "value" "of" ident ")"
]

rename: [
| ident "into" ident
]

by_arg_tac: [
| "by" ltac_expr3
|
]

in_clause: [
| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ )
| "*" "|-" OPT concl_occ
| "*" OPT ( "at" occs_nums )
]

concl_occ: [
| "*" OPT ( "at" occs_nums )
]

hypident_occ: [
| hypident OPT ( "at" occs_nums )
]

hypident: [
| ident
| "(" "type" "of" ident ")"
| "(" "value" "of" ident ")"
]

as_ipat: [
| "as" simple_intropattern
|
]

or_and_intropattern_loc: [
| or_and_intropattern
| ident
]

as_or_and_ipat: [
| "as" or_and_intropattern_loc
|
]

eqn_ipat: [
| "eqn" ":" naming_intropattern
| "_eqn" ":" naming_intropattern
| "_eqn"
|
]

as_name: [
| "as" ident
|
]

by_tactic: [
| "by" ltac_expr3
|
]

rewriter: [
| "!" constr_with_bindings_arg
| [ "?" | "?" ] constr_with_bindings_arg
| num "!" constr_with_bindings_arg
| num [ "?" | "?" ] constr_with_bindings_arg
| num constr_with_bindings_arg
| constr_with_bindings_arg
]

oriented_rewriter: [
| orient rewriter
]

induction_clause: [
| destruction_arg as_or_and_ipat eqn_ipat opt_clause
]

induction_clause_list: [
| LIST1 induction_clause SEP "," OPT ( "using" constr_with_bindings ) opt_clause
]

auto_using: [
| "using" LIST1 one_term SEP ","
|
]

intropattern_list_opt: [
| LIST0 intropattern
]

or_and_intropattern: [
| "[" intropattern_or_list_or "]"
| "(" LIST0 simple_intropattern SEP "," ")"
| "(" simple_intropattern "&" LIST1 simple_intropattern SEP "&" ")"
]

intropattern_or_list_or: [
| intropattern_or_list_or "|" intropattern_list_opt
| intropattern_list_opt
]

equality_intropattern: [
| "->"
| "<-"
| "[=" intropattern_list_opt "]"
]

naming_intropattern: [
| "?" ident
| "?"
| ident
]

intropattern: [
| simple_intropattern
| "*"
| "**"
]

simple_intropattern: [
| simple_intropattern_closed LIST0 [ "%" term0 ]
]

simple_intropattern_closed: [
| or_and_intropattern
| equality_intropattern
| "_"
| naming_intropattern
]

simple_binding: [
| "(" ident ":=" term ")"
| "(" num ":=" term ")"
]

bindings: [
| LIST1 simple_binding
| LIST1 one_term
]

comparison: [
| "="
| "<"
| "<="
| ">"
| ">="
]

hintbases: [
| "with" "*"
| "with" LIST1 ident
|
]

bindings_with_parameters: [
| "(" ident LIST0 simple_binder ":=" term ")"
]

clause_dft_concl: [
| "in" in_clause
| OPT ( "at" occs_nums )
|
]

clause_dft_all: [
| "in" in_clause
|
]

opt_clause: [
| "in" in_clause
| "at" occs_nums
|
]

in_hyp_list: [
| "in" LIST1 ident
|
]

in_hyp_as: [
| "in" ident as_ipat
|
]

simple_binder: [
| name
| "(" LIST1 name ":" term ")"
]

fixdecl: [
| "(" ident LIST0 simple_binder struct_annot ":" term ")"
]

struct_annot: [
| "{" "struct" name "}"
|
]

cofixdecl: [
| "(" ident LIST0 simple_binder ":" term ")"
]

constr_with_bindings: [
| one_term with_bindings
]

with_bindings: [
| "with" bindings
|
]

destruction_arg: [
| num
| constr_with_bindings
| constr_with_bindings_arg
]

constr_with_bindings_arg: [
| ">" constr_with_bindings
| constr_with_bindings
]

quantified_hypothesis: [
| ident
| num
]

conversion: [
| one_term
| one_term "with" one_term
| one_term "at" occs_nums "with" one_term
]

firstorder_using: [
| "using" qualid
| "using" qualid "," LIST1 qualid SEP ","
| "using" qualid qualid LIST0 qualid
|
]

fun_ind_using: [
| "using" constr_with_bindings      (* funind plugin *)
|      (* funind plugin *)
]

with_names: [
| "as" simple_intropattern      (* funind plugin *)
|      (* funind plugin *)
]

occurrences: [
| LIST1 int
| ident
]

rewstrategy: [
| one_term
| "<-" one_term
| "fail"
| "id"
| "refl"
| "progress" rewstrategy
| "try" rewstrategy
| rewstrategy ";" rewstrategy
| "choice" rewstrategy rewstrategy
| "repeat" rewstrategy
| "any" rewstrategy
| "subterm" rewstrategy
| "subterms" rewstrategy
| "innermost" rewstrategy
| "outermost" rewstrategy
| "bottomup" rewstrategy
| "topdown" rewstrategy
| "hints" ident
| "terms" LIST0 one_term
| "eval" red_expr
| "fold" one_term
| "(" rewstrategy ")"
| "old_hints" ident
]

ltac_expr: [
| binder_tactic
| ltac_expr4
]

binder_tactic: [
| "fun" LIST1 fun_var "=>" ltac_expr
| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
| "info" ltac_expr
]

fun_var: [
| ident
| "_"
]

let_clause: [
| ident ":=" ltac_expr
| "_" ":=" ltac_expr
| ident LIST1 fun_var ":=" ltac_expr
]

ltac_expr4: [
| ltac_expr3 ";" binder_tactic
| ltac_expr3 ";" ltac_expr3
| ltac_expr3 ";" "[" OPT multi_goal_tactics "]"
| ltac_expr3
| ltac_expr3 ";" "[" ">" OPT multi_goal_tactics "]"
]

multi_goal_tactics: [
| OPT ltac_expr "|" multi_goal_tactics
| ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or
| ltac_expr
]

ltac_expr_opt: [
| OPT ltac_expr
]

ltac_expr_opt_list_or: [
| ltac_expr_opt_list_or "|" ltac_expr_opt
| ltac_expr_opt
| ltac_expr_opt_list_or "|" OPT ltac_expr
| OPT ltac_expr
]

ltac_expr3: [
| "try" ltac_expr3
| "do" int_or_var ltac_expr3
| "timeout" int_or_var ltac_expr3
| "time" OPT string ltac_expr3
| "repeat" ltac_expr3
| "progress" ltac_expr3
| "once" ltac_expr3
| "exactly_once" ltac_expr3
| "infoH" ltac_expr3
| "abstract" ltac_expr2
| "abstract" ltac_expr2 "using" ident
| only_selector ltac_expr3
| ltac_expr2
]

only_selector: [
| "only" selector ":"
]

selector: [
| LIST1 range_selector SEP ","
| "[" ident "]"
]

range_selector: [
| num "-" num
| num
]

ltac_expr2: [
| ltac_expr1 "+" binder_tactic
| ltac_expr1 "+" ltac_expr2
| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
| ltac_expr1 "||" binder_tactic
| ltac_expr1 "||" ltac_expr2
| ltac_expr1
]

ltac_expr1: [
| ltac_match_term
| "first" "[" LIST0 ltac_expr SEP "|" "]"
| "solve" "[" LIST0 ltac_expr SEP "|" "]"
| "idtac" LIST0 message_token
| failkw OPT int_or_var LIST0 message_token
| ltac_match_goal
| simple_tactic
| tactic_arg
| qualid LIST0 tactic_arg_compat
| ltac_expr0
]

message_token: [
| ident
| string
| int
]

failkw: [
| "fail"
| "gfail"
]

tactic_arg: [
| "eval" red_expr "in" term
| "context" ident "[" term "]"
| "type" "of" term
| "fresh" LIST0 fresh_id
| "type_term" one_term
| "numgoals"
]

fresh_id: [
| string
| qualid
]

tactic_arg_compat: [
| tactic_arg
| term
| "()"
]

ltac_expr0: [
| "(" ltac_expr ")"
| "[>" OPT multi_goal_tactics "]"
| tactic_atom
]

tactic_atom: [
| int
| qualid
| "()"
]

toplevel_selector: [
| selector ":"
| "all" ":"
| "!" ":"
]

ltac_match_term: [
| match_key ltac_expr "with" OPT "|" LIST1 match_rule SEP "|" "end"
]

match_key: [
| "match"
| "multimatch"
| "lazymatch"
]

match_rule: [
| [ match_pattern | "_" ] "=>" ltac_expr
]

match_pattern: [
| "context" OPT ident "[" term "]"
| term
]

ltac_match_goal: [
| match_key OPT "reverse" "goal" "with" OPT "|" LIST1 match_context_rule SEP "|" "end"
]

match_context_rule: [
| LIST0 match_hyp SEP "," "|-" match_pattern "=>" ltac_expr
| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]" "=>" ltac_expr
| "_" "=>" ltac_expr
]

match_hyp: [
| name ":" match_pattern
| name ":=" OPT ( "[" match_pattern "]" ":" ) match_pattern
]