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

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
]

record_fields: [
| record_field ";" record_fields
| record_field
|
]

record_field: [
| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) record_binder OPT [ "|" num ] decl_notation
]

decl_notation: [
| "where" LIST1 one_decl_notation SEP "and"
|
]

one_decl_notation: [
| string ":=" term1_extended OPT [ ":" ident ]
]

record_binder: [
| name
| name record_binder_body
]

record_binder_body: [
| LIST0 binder of_type_with_opt_coercion term
| LIST0 binder of_type_with_opt_coercion term ":=" term
| LIST0 binder ":=" term
]

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

attribute: [
| ident attribute_value
]

attribute_value: [
| "=" string
| "(" LIST0 attribute SEP "," ")"
|
]

qualid: [
| ident LIST0 field_ident
]

field_ident: [
| "." ident
]

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

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

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

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

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 ( ":" term ) ":=" term
]

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

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

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

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

term_let: [
| "let" name OPT ( ":" term ) ":=" term "in" term
| "let" name LIST1 binder OPT ( ":" term ) ":=" 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 ":" term ")"
| "(" name OPT ( ":" term ) ":=" term ")"
| "{" LIST1 name OPT ( ":" term ) "}"
| "`(" LIST1 typeclass_constraint SEP "," ")"
| "`{" LIST1 typeclass_constraint SEP "," "}"
| "'" pattern0
| "(" name ":" term "|" term ")"
]

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 ":" term LIST0 [ "with" ident_decl LIST0 binder ":" term ]
| assumption_token inline assum_list
| assumptions_token inline assum_list
| def_token ident_decl def_body
| "Let" ident def_body
| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
| "Fixpoint" LIST1 fix_definition SEP "with"
| "Let" "Fixpoint" LIST1 fix_definition SEP "with"
| "CoFixpoint" LIST1 cofix_definition SEP "with"
| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with"
| "Scheme" LIST1 scheme SEP "with"
| "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 ( ":" term ) OPT [ ":=" term ] decl_notation
]

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_token: [
| "Definition"
| "Example"
| "SubClass"
]

assumption_token: [
| "Hypothesis"
| "Variable"
| "Axiom"
| "Parameter"
| "Conjecture"
]

assumptions_token: [
| "Hypotheses"
| "Variables"
| "Axioms"
| "Parameters"
| "Conjectures"
]

inline: [
| "Inline" "(" num ")"
| "Inline"
|
]

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

ident_decl: [
| ident OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] )
]

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

cumulativity_token: [
| "Cumulative"
| "NonCumulative"
]

private_token: [
| "Private"
|
]

def_body: [
| LIST0 binder ":=" reduce term
| LIST0 binder ":" term ":=" reduce term
| LIST0 binder ":" term
]

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

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

strategy_flag: [
| LIST1 red_flags
| delta_flag
]

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

delta_flag: [
| "-" "[" LIST1 smart_global "]"
| "[" LIST1 smart_global "]"
|
]

ref_or_pattern_occ: [
| smart_global occs
| term1_extended occs
]

unfold_occ: [
| smart_global occs
]

opt_constructors_or_fields: [
| ":=" constructor_list_or_record_decl
|
]

inductive_definition: [
| opt_coercion ident_decl LIST0 binder OPT [ ":" term ] opt_constructors_or_fields decl_notation
]

opt_coercion: [
| ">"
|
]

constructor_list_or_record_decl: [
| "|" LIST1 constructor SEP "|"
| ident constructor_type "|" LIST0 constructor SEP "|"
| ident constructor_type
| ident "{" record_fields "}"
| "{" record_fields "}"
|
]

assum_list: [
| LIST1 assum_coe
| simple_assum_coe
]

assum_coe: [
| "(" simple_assum_coe ")"
]

simple_assum_coe: [
| LIST1 ident_decl of_type_with_opt_coercion term
]

constructor_type: [
| LIST0 binder [ of_type_with_opt_coercion term | ]
]

constructor: [
| ident constructor_type
]

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

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

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

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

smart_global: [
| qualid
| by_notation
]

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

gallina_ext: [
| "Module" export_token ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) of_module_type is_module_expr
| "Module" "Type" ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) LIST0 ( "<:" module_type_inl ) is_module_type
| "Declare" "Module" export_token ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) ":" module_type_inl
| "Section" ident
| "Chapter" ident
| "End" ident
| "Collection" ident ":=" section_subset_expr
| "Require" export_token LIST1 qualid
| "From" qualid "Require" 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_global
| "Opaque" LIST1 smart_global
| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
| "Canonical" OPT "Structure" qualid OPT [ OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body ]
| "Canonical" OPT "Structure" by_notation
| "Coercion" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body
| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
| "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr
| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
| "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_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] 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
]

class_rawexpr: [
| "Funclass"
| "Sortclass"
| smart_global
]

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

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

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

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

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

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

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

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

module_expr: [
| module_expr_atom
| module_expr module_expr_atom
]

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

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

with_declaration: [
| "Definition" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) ":=" term
| "Module" qualid ":=" qualid
]

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

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

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
]

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

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" printable
| "Print" smart_global OPT ( "@{" LIST0 name "}" )
| "Print" "Module" "Type" qualid
| "Print" "Module" qualid
| "Print" "Namespace" dirpath
| "Inspect" num
| "Add" "ML" "Path" string
| "Add" "Rec" "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" term1_extended "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" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Setoid" term1_extended term1_extended term1_extended "as" ident
| "Add" "Parametric" "Setoid" LIST0 binder ":" term1_extended term1_extended term1_extended "as" ident
| "Add" "Morphism" term1_extended ":" ident
| "Declare" "Morphism" term1_extended ":" ident
| "Add" "Morphism" term1_extended "with" "signature" term "as" ident
| "Add" "Parametric" "Morphism" LIST0 binder ":" term1_extended "with" "signature" term "as" ident
| "Grab" "Existential" "Variables"
| "Unshelve"
| "Declare" "Equivalent" "Keys" term1_extended term1_extended
| "Print" "Equivalent" "Keys"
| "Optimize" "Proof"
| "Optimize" "Heap"
| "Reset" "Ltac" "Profile"
| "Show" "Ltac" "Profile"
| "Show" "Ltac" "Profile" "CutOff" int
| "Show" "Ltac" "Profile" string
| "Add" "InjTyp" term1_extended      (* micromega plugin *)
| "Add" "BinOp" term1_extended      (* micromega plugin *)
| "Add" "UnOp" term1_extended      (* micromega plugin *)
| "Add" "CstOp" term1_extended      (* micromega plugin *)
| "Add" "BinRel" term1_extended      (* micromega plugin *)
| "Add" "PropOp" term1_extended      (* micromega plugin *)
| "Add" "PropUOp" term1_extended      (* micromega plugin *)
| "Add" "Spec" term1_extended      (* micromega plugin *)
| "Add" "BinOpSpec" term1_extended      (* micromega plugin *)
| "Add" "UnOpSpec" term1_extended      (* micromega plugin *)
| "Add" "Saturate" term1_extended      (* 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 ":" term1_extended 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" LIST1 tacdef_body SEP "with"
| "Print" "Ltac" "Signatures"
| "Set" "Firstorder" "Solver" ltac_expr
| "Print" "Firstorder" "Solver"
| "Function" LIST1 fix_definition SEP "with"      (* funind plugin *)
| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
| "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 term1_extended ":" LIST0 ident
| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr ":" LIST0 ident
| "Hint" "Rewrite" orient LIST1 term1_extended
| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr
| "Derive" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
| "Derive" "Inversion_clear" ident "with" term1_extended
| "Derive" "Inversion" ident "with" term1_extended "Sort" sort_family
| "Derive" "Inversion" ident "with" term1_extended
| "Derive" "Dependent" "Inversion" ident "with" term1_extended "Sort" sort_family
| "Derive" "Dependent" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
| "Declare" "Left" "Step" term1_extended
| "Declare" "Right" "Step" term1_extended
| "Print" "Rings"      (* setoid_ring plugin *)
| "Add" "Field" ident ":" term1_extended OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
| "Print" "Fields"      (* setoid_ring plugin *)
| "Numeral" "Notation" qualid qualid qualid ":" ident numnotoption
| "String" "Notation" qualid qualid qualid ":" ident
]

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

printable: [
| "Term" smart_global OPT ( "@{" LIST0 name "}" )
| "All"
| "Section" qualid
| "Grammar" ident
| "Custom" "Grammar" ident
| "LoadPath" OPT dirpath
| "Modules"
| "Libraries"
| "ML" "Path"
| "ML" "Modules"
| "Debug" "GC"
| "Graph"
| "Classes"
| "TypeClasses"
| "Instances" smart_global
| "Coercions"
| "Coercion" "Paths" class_rawexpr class_rawexpr
| "Canonical" "Projections"
| "Typing" "Flags"
| "Tables"
| "Options"
| "Hint"
| "Hint" smart_global
| "Hint" "*"
| "HintDb" ident
| "Scopes"
| "Scope" ident
| "Visibility" OPT ident
| "Implicit" smart_global
| [ "Sorted" | ] "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
| "Assumptions" smart_global
| "Opaque" "Dependencies" smart_global
| "Transparent" "Dependencies" smart_global
| "All" "Dependencies" smart_global
| "Strategy" smart_global
| "Strategies"
| "Registered"
]

dirpath: [
| ident
| dirpath field_ident
]

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

option_ref_value: [
| qualid
| string
]

as_dirpath: [
| OPT [ "as" dirpath ]
]

comment: [
| term1_extended
| string
| num
]

reference_or_constr: [
| qualid
| term1_extended
]

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 term1_extended "=>" 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" term1_extended      (* setoid_ring plugin *)
| "abstract"      (* setoid_ring plugin *)
| "morphism" term1_extended      (* setoid_ring plugin *)
| "constants" "[" ltac_expr "]"      (* setoid_ring plugin *)
| "closed" "[" LIST1 qualid "]"      (* setoid_ring plugin *)
| "preprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
| "postprocess" "[" ltac_expr "]"      (* setoid_ring plugin *)
| "setoid" term1_extended term1_extended      (* setoid_ring plugin *)
| "sign" term1_extended      (* setoid_ring plugin *)
| "power" term1_extended "[" LIST1 qualid "]"      (* setoid_ring plugin *)
| "power_tac" term1_extended "[" ltac_expr "]"      (* setoid_ring plugin *)
| "div" term1_extended      (* setoid_ring plugin *)
]

field_mod: [
| ring_mod      (* setoid_ring plugin *)
| "completeness" term1_extended      (* 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_global OPT ( "@{" LIST0 name "}" ) "."
| "SearchHead" term1_extended in_or_out_modules "."
| "SearchPattern" term1_extended in_or_out_modules "."
| "SearchRewrite" term1_extended in_or_out_modules "."
| "Search" searchabout_query searchabout_queries "."
| "SearchAbout" searchabout_query searchabout_queries "."
| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
]

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

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_rawexpr
| "Infix" string ":=" term1_extended [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" ident ]
| "Notation" ident LIST0 ident ":=" term1_extended only_parsing
| "Notation" string ":=" term1_extended [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" ident ]
| "Format" "Notation" string string string
| "Reserved" "Infix" string [ "(" LIST1 syntax_modifier SEP "," ")" | ]
| "Reserved" "Notation" string [ "(" LIST1 syntax_modifier SEP "," ")" | ]
]

only_parsing: [
| "(" "only" "parsing" ")"
|
]

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
| ident "at" level constr_as_binder_kind
| ident constr_as_binder_kind
| ident syntax_extension_type
]

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

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

simple_tactic: [
| "reflexivity"
| "exact" term1_extended
| "assumption"
| "etransitivity"
| "cut" term1_extended
| "exact_no_check" term1_extended
| "vm_cast_no_check" term1_extended
| "native_cast_no_check" term1_extended
| "casetype" term1_extended
| "elimtype" term1_extended
| "lapply" term1_extended
| "transitivity" term1_extended
| "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" term1_extended
| "replace" term1_extended "with" term1_extended clause_dft_concl by_arg_tac
| "replace" "->" term1_extended clause_dft_concl
| "replace" "<-" term1_extended clause_dft_concl
| "replace" term1_extended 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 term1_extended
| "dependent" "rewrite" orient term1_extended "in" ident
| "cutrewrite" orient term1_extended
| "cutrewrite" orient term1_extended "in" ident
| "decompose" "sum" term1_extended
| "decompose" "record" term1_extended
| "absurd" term1_extended
| "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 term1_extended "in" ident "at" occurrences by_arg_tac
| "rewrite" "*" orient term1_extended "at" occurrences "in" ident by_arg_tac
| "rewrite" "*" orient term1_extended "in" ident by_arg_tac
| "rewrite" "*" orient term1_extended "at" occurrences by_arg_tac
| "rewrite" "*" orient term1_extended by_arg_tac
| "refine" term1_extended
| "simple" "refine" term1_extended
| "notypeclasses" "refine" term1_extended
| "simple" "notypeclasses" "refine" term1_extended
| "solve_constraints"
| "subst" LIST1 ident
| "subst"
| "simple" "subst"
| "evar" "(" ident ":" term ")"
| "evar" term1_extended
| "instantiate" "(" ident ":=" term ")"
| "instantiate" "(" int ":=" term ")" hloc
| "instantiate"
| "stepl" term1_extended "by" ltac_expr
| "stepl" term1_extended
| "stepr" term1_extended "by" ltac_expr
| "stepr" term1_extended
| "generalize_eqs" ident
| "dependent" "generalize_eqs" ident
| "generalize_eqs_vars" ident
| "dependent" "generalize_eqs_vars" ident
| "specialize_eqs" ident
| "hresolve_core" "(" ident ":=" term1_extended ")" "at" int_or_var "in" term1_extended
| "hresolve_core" "(" ident ":=" term1_extended ")" "in" term1_extended
| "hget_evar" int_or_var
| "destauto"
| "destauto" "in" ident
| "transparent_abstract" ltac_expr3
| "transparent_abstract" ltac_expr3 "using" ident
| "constr_eq" term1_extended term1_extended
| "constr_eq_strict" term1_extended term1_extended
| "constr_eq_nounivs" term1_extended term1_extended
| "is_evar" term1_extended
| "has_evar" term1_extended
| "is_var" term1_extended
| "is_fix" term1_extended
| "is_cofix" term1_extended
| "is_ind" term1_extended
| "is_constructor" term1_extended
| "is_proj" term1_extended
| "is_const" term1_extended
| "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 term1_extended "]" term1_extended
| "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" term1_extended
| "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 term1_extended "]" 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" term1_extended term1_extended
| "unify" term1_extended term1_extended "with" ident
| "convert_concl_no_check" term1_extended
| "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 term1_extended
| "not_evar" term1_extended
| "is_ground" term1_extended
| "autoapply" term1_extended "using" ident
| "autoapply" term1_extended "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" term1_extended
| "setoid_etransitivity"
| "decide" "equality"
| "compare" term1_extended term1_extended
| "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" term1_extended as_name
| "epose" bindings_with_parameters
| "epose" term1_extended as_name
| "set" bindings_with_parameters clause_dft_concl
| "set" term1_extended as_name clause_dft_concl
| "eset" bindings_with_parameters clause_dft_concl
| "eset" term1_extended as_name clause_dft_concl
| "remember" term1_extended as_name eqn_ipat clause_dft_all
| "eremember" term1_extended 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" term1_extended as_ipat by_tactic
| "eassert" term1_extended as_ipat by_tactic
| "pose" "proof" term as_ipat
| "epose" "proof" term as_ipat
| "enough" term1_extended as_ipat by_tactic
| "eenough" term1_extended as_ipat by_tactic
| "generalize" term1_extended
| "generalize" term1_extended LIST1 term1_extended
| "generalize" term1_extended occs 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" term1_extended ]
| "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" term1_extended in_hyp_list
| "red" clause_dft_concl
| "hnf" clause_dft_concl
| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl
| "cbv" strategy_flag clause_dft_concl
| "cbn" strategy_flag clause_dft_concl
| "lazy" strategy_flag clause_dft_concl
| "compute" 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 term1_extended 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 term1_extended
| "congruence" int "with" LIST1 term1_extended
| "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 term1_extended fun_ind_using with_names      (* funind plugin *)
| "soft" "functional" "induction" LIST1 term1_extended fun_ind_using with_names      (* funind plugin *)
| "myred"      (* micromega 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 *)
| "iter_specs" ltac_expr      (* micromega plugin *)
| "zify_op"      (* micromega plugin *)
| "saturate"      (* micromega plugin *)
| "nsatz_compute" term1_extended      (* nsatz plugin *)
| "omega"      (* omega plugin *)
| "omega" "with" LIST1 ident      (* omega plugin *)
| "omega" "with" "*"      (* omega plugin *)
| "protect_fv" string "in" ident      (* setoid_ring plugin *)
| "protect_fv" string      (* setoid_ring plugin *)
| "ring_lookup" ltac_expr0 "[" LIST0 term1_extended "]" LIST1 term1_extended      (* setoid_ring plugin *)
| "field_lookup" ltac_expr "[" LIST0 term1_extended "]" LIST1 term1_extended      (* setoid_ring plugin *)
]

int_or_var: [
| int
| ident
]

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: [
| in_clause
| "*" occs
| "*" "|-" concl_occ
| LIST0 hypident_occ SEP "," "|-" concl_occ
| LIST0 hypident_occ SEP ","
]

occs: [
| "at" occs_nums
|
]

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

pattern_occ: [
| term1_extended occs
]

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

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

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

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

hypident_occ: [
| hypident occs
]

clause_dft_concl: [
| "in" in_clause
| occs
|
]

clause_dft_all: [
| "in" in_clause
|
]

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

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

num_or_var: [
| num
| ident
]

concl_occ: [
| "*" occs
|
]

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: [
| term1_extended 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: [
| term1_extended
| term1_extended "with" term1_extended
| term1_extended "at" occs_nums "with" term1_extended
]

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

ltac_expr: [
| binder_tactic
| ltac_expr4
]

binder_tactic: [
| "fun" LIST1 fun_var "=>" ltac_expr
| "let" [ "rec" | ] LIST1 let_clause SEP "with" "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 ";" "[" multi_goal_tactics "]"
| ltac_expr3 ";" "[" ">" multi_goal_tactics "]"
| ltac_expr3
]

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
]

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 [ 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" term1_extended
| "numgoals"
]

fresh_id: [
| string
| qualid
]

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

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

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

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

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

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

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

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
]