(* Defines the order to apply to editedGrammar to get the final grammar for the doc.
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

tactic_mode: [
| OPT ( toplevel_selector ":" ) "{"
]

term: [
| term_forall_or_fun
| term_let
| term_if
| term_fix
| term_cofix
| term100
]

term100: [
| term_cast
| term10
]

term10: [
| term_application
| one_term
]

one_term: [
| term_explicit
| term1
]

term1: [
| term_projection
| term_scope
| term0
]

term0: [
| qualid_annotated
| sort
| primitive_notations
| term_evar
| term_match
| term_record
| term_generalizing
| term_ltac
| "(" term ")"
]

qualid_annotated: [
| qualid OPT univ_annot
]

term_ltac: [
| "ltac" ":" "(" ltac_expr ")"
]

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

term_scope: [
| term0 "%" scope_key
]

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

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

term_application: [
| term1 LIST1 arg
| "@" qualid_annotated LIST1 term1
]

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

term_explicit: [
| "@" qualid_annotated
]

primitive_notations: [
| numeral
| string
]

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: [
| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
]

int: [
| OPT "-" num
]

num: [
| [ decnum | hexnum ]
]

decnum: [
| digit LIST0 [ digit | "_" ]
]

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

hexnum: [
| [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
]

hexdigit: [
| [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ]
]

ident: [
| first_letter LIST0 subsequent_letter
]

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

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

firstorder_rhs: [
| OPT firstorder_using
| "with" LIST1 ident
| OPT firstorder_using "with" LIST1 ident
]

where: [
| "at" "top"
| "at" "bottom"
| "after" ident
| "before" ident
]

REACHABLE: [
| command
| simple_tactic
| NOTINRSTS
]

NOTINRSTS: [
| simple_tactic
| REACHABLE
| NOTINRSTS
]

document: [
| LIST0 sentence
]

nonterminal: [
]

sentence: [
| OPT attributes command "."
| OPT attributes OPT ( num ":" ) query_command "."
| OPT attributes OPT ( toplevel_selector ":" ) ltac_expr [ "." | "..." ]
| control_command
]

control_command: [
]

query_command: [
]

attributes: [
| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
]

attribute: [
| ident OPT attr_value
]

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

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

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_if: [
| "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" 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
]

term_forall_or_fun: [
| "forall" open_binders "," term
| "fun" open_binders "=>" term
]

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

name: [
| "_"
| ident
]

binder: [
| name
| "(" LIST1 name ":" type ")"
| "(" name OPT ( ":" type ) ":=" term ")"
| implicit_binders
| generalizing_binder
| "(" name ":" type "|" term ")"
| "'" pattern0
]

implicit_binders: [
| "{" LIST1 name OPT ( ":" type ) "}"
| "[" LIST1 name OPT ( ":" type ) "]"
]

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

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

term_generalizing: [
| "`{" term "}"
| "`(" term ")"
]

term_cast: [
| term10 "<:" type
| term10 "<<:" type
| term10 ":" type
| 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 "%" scope_key
| pattern0
]

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

vernac_aux: [
| command "."
| tactic_mode "."
| subprf
]

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

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

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

strategy_flag: [
| LIST1 red_flags
| delta_flag
]

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

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

occs_nums: [
| LIST1 [ num | ident ]
| "-" [ num | ident ] LIST0 int_or_var
]

int_or_var: [
| int
| ident
]

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

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

variant_definition: [
| ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT "|" LIST1 constructor SEP "|" OPT decl_notations
]

record_definition: [
| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations
]

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

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

term_record: [
| "{|" LIST0 field_def "|}"
]

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

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 "{" LIST0 record_field SEP ";" "}"
]

constructor: [
| ident LIST0 binder OPT of_type
]

filtered_import: [
| qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
]

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

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

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

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

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

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

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

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
]

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

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

module_expr_inl: [
| "!" LIST1 module_expr_atom
| LIST1 module_expr_atom OPT functor_app_annot
]

reference: [
| qualid
| string OPT [ "%" scope_key ]
]

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

arg_specs: [
| argument_spec
| "/"
| "&"
| "(" LIST1 argument_spec ")" OPT ( "%" scope_key )
| "[" LIST1 argument_spec "]" OPT ( "%" scope_key )
| "{" LIST1 argument_spec "}" OPT ( "%" scope_key )
]

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

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

scope: [
| scope_name
| scope_key
]

scope_name: [
| ident
]

scope_key: [
| ident
]

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

strategy_level_or_var: [
| strategy_level
| ident
]

reserv_list: [
| LIST1 ( "(" simple_reserv ")" )
| simple_reserv
]

simple_reserv: [
| LIST1 ident ":" type
]

command: [
| "Goal" term
| "Pwd"
| "Cd" OPT string
| "Load" OPT "Verbose" [ string | ident ]
| "Declare" "ML" "Module" LIST1 string
| "Locate" reference
| "Locate" "Term" reference
| "Locate" "Module" qualid
| "Info" num ltac_expr
| "Locate" "Ltac" qualid
| "Locate" "Library" qualid
| "Locate" "File" string
| "Add" "LoadPath" string "as" dirpath
| "Add" "Rec" "LoadPath" string "as" dirpath
| "Remove" "LoadPath" string
| "Type" term
| "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" reference
| "Print" "Coercions"
| "Print" "Coercion" "Paths" class class
| "Print" "Canonical" "Projections" LIST0 reference
| "Print" "Typing" "Flags"
| "Print" "Tables"
| "Print" "Options"
| "Print" "Hint"
| "Print" "Hint" reference
| "Print" "Hint" "*"
| "Print" "HintDb" ident
| "Print" "Scopes"
| "Print" "Scope" scope_name
| "Print" "Visibility" OPT scope_name
| "Print" "Implicit" reference
| "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string
| "Print" "Assumptions" reference
| "Print" "Opaque" "Dependencies" reference
| "Print" "Transparent" "Dependencies" reference
| "Print" "All" "Dependencies" reference
| "Print" "Strategy" reference
| "Print" "Strategies"
| "Print" "Registered"
| "Print" OPT "Term" reference OPT univ_name_list
| "Print" "Module" "Type" qualid
| "Print" "Module" qualid
| "Print" "Namespace" dirpath
| "Inspect" num
| "Add" "ML" "Path" string
| OPT "Export" "Set" setting_name
| "Print" "Table" setting_name
| "Add" setting_name LIST1 [ qualid | string ]
| "Test" setting_name OPT ( "for" LIST1 [ qualid | string ] )
| "Remove" setting_name LIST1 [ qualid | string ]
| "Write" "State" [ ident | string ]
| "Restore" "State" [ ident | string ]
| "Reset" "Initial"
| "Reset" ident
| "Back" OPT num
| "Debug" [ "On" | "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" OPT [ "All" | ident ]
| "Existential" num OPT ( ":" term ) ":=" term
| "Admitted"
| "Qed"
| "Save" ident
| "Defined" OPT ident
| "Restart"
| "Undo" OPT ( OPT "To" num )
| "Focus" OPT num
| "Unfocus"
| "Unfocused"
| "Show" OPT [ ident | num ]
| "Show" "Existentials"
| "Show" "Universes"
| "Show" "Conjectures"
| "Show" "Proof" OPT ( "Diffs" OPT "removed" )
| "Show" "Intro"
| "Show" "Intros"
| "Show" "Match" qualid
| "Guarded"
| "Create" "HintDb" ident OPT "discriminated"
| "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
| "Hint" hint OPT ( ":" LIST1 ident )
| "Comments" LIST0 [ one_term | string | num ]
| "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
| "Declare" "Scope" scope_name
| "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
| "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr )
| "Solve" "Obligation" int OPT ( "of" ident ) "with" ltac_expr
| "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr )
| "Solve" "All" "Obligations" OPT ( "with" ltac_expr )
| "Admit" "Obligations" OPT ( "of" ident )
| "Obligation" "Tactic" ":=" ltac_expr
| "Show" "Obligation" "Tactic"
| "Obligations" OPT ( "of" ident )
| "Preterm" OPT ( "of" ident )
| "Add" "Relation" one_term one_term OPT ( "reflexivity" "proved" "by" one_term ) OPT ( "symmetry" "proved" "by" one_term ) OPT ( "transitivity" "proved" "by" one_term ) "as" ident
| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term OPT ( "reflexivity" "proved" "by" one_term ) OPT ( "symmetry" "proved" "by" one_term ) OPT ( "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" OPT [ "CutOff" int | 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 "]" OPT ( ":" LIST1 ident )
| "Typeclasses" "Transparent" LIST0 qualid
| "Typeclasses" "Opaque" LIST0 qualid
| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) 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
| "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 "=>" [ ident | string ]      (* extraction plugin *)
| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ]      (* extraction plugin *)
| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string      (* extraction plugin *)
| "Show" "Extraction"      (* extraction plugin *)
| "Functional" "Case" fun_scheme_arg      (* funind plugin *)
| "Generate" "graph" "for" qualid      (* funind plugin *)
| "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" ltac_expr ) OPT ( ":" LIST0 ident )
| "Derive" "Inversion_clear" ident "with" one_term OPT ( "Sort" sort_family )
| "Derive" "Inversion" ident "with" one_term OPT ( "Sort" sort_family )
| "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 ":" scope_name OPT numeral_modifier
| "String" "Notation" qualid qualid qualid ":" scope_name
| "SubClass" ident_decl def_body
| 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_decl def_body
| "Inductive" 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" OPT ( ident ":=" ) scheme_kind LIST0 ( "with" OPT ( ident ":=" ) scheme_kind )
| "Combined" "Scheme" ident "from" LIST1 ident SEP ","
| "Register" qualid "as" qualid
| "Register" "Inline" qualid
| "Primitive" ident OPT [ ":" term ] ":=" "#" ident
| "Universe" LIST1 ident
| "Universes" LIST1 ident
| "Constraint" LIST1 univ_constraint SEP ","
| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
| "Variant" variant_definition LIST0 ( "with" variant_definition )
| [ "Record" | "Structure" ] record_definition LIST0 ( "with" record_definition )
| "Class" inductive_definition LIST0 ( "with" inductive_definition )
| "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder OPT of_module_type OPT ( ":=" LIST1 module_expr_inl SEP "<+" )
| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
| "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
| "Section" ident
| "End" ident
| "Collection" ident ":=" section_subset_expr
| "Require" OPT [ "Import" | "Export" ] LIST1 qualid
| "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid
| "Import" LIST1 filtered_import
| "Export" LIST1 filtered_import
| "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
| "Include" "Type" LIST1 module_type_inl SEP "<+"
| "Transparent" LIST1 reference
| "Opaque" LIST1 reference
| "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ]
| "Canonical" OPT "Structure" ident_decl def_body
| "Canonical" OPT "Structure" reference
| "Coercion" qualid OPT univ_decl def_body
| "Identity" "Coercion" ident ":" class ">->" class
| "Coercion" reference ":" class ">->" class
| "Context" LIST1 binder
| "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ]
| "Existing" "Instance" qualid OPT hint_info
| "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
| "Existing" "Class" qualid
| "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
| "Implicit" [ "Type" | "Types" ] reserv_list
| "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
| "Set" setting_name OPT [ int | string ]
| "Unset" setting_name
| "Open" "Scope" scope
| "Close" "Scope" scope
| "Delimit" "Scope" scope_name "with" scope_key
| "Undelimit" "Scope" scope_name
| "Bind" "Scope" scope_name "with" LIST1 class
| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" scope_name ]
| "Format" "Notation" string string string
| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ]
| "Eval" red_expr "in" term
| "Compute" term
| "Check" term
| "About" reference OPT univ_name_list
| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Time" sentence
| "Redirect" string sentence
| "Timeout" num sentence
| "Fail" sentence
| "Drop"
| "Quit"
| "BackTo" num
| "Show" "Goal" num "at" num
]

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

setting_name: [
| LIST1 ident
]

search_query: [
| search_item
| "-" search_query
| "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
]

search_item: [
| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key )
| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term
| "is" ":" logical_kind
]

logical_kind: [
| [ thm_token | assumption_token ]
| [ "Definition" | "Example" | "Context" | "Primitive" ]
| [ "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
| [ "Field" | "Method" ]
]

univ_name_list: [
| "@{" LIST0 name "}"
]

hint: [
| "Resolve" LIST1 [ qualid | one_term ] OPT hint_info
| "Resolve" "->" LIST1 qualid OPT num
| "Resolve" "<-" LIST1 qualid OPT num
| "Immediate" LIST1 [ qualid | one_term ]
| "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
]

tacdef_body: [
| qualid LIST0 name [ ":=" | "::=" ] ltac_expr
]

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

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

numeral_modifier: [
| "(" "warning" "after" numeral ")"
| "(" "abstract" "after" numeral ")"
]

hints_path: [
| "(" hints_path ")"
| hints_path "*"
| "emp"
| "eps"
| hints_path "|" hints_path
| LIST1 qualid
| "_"
| hints_path hints_path
]

eauto_search_strategy_name: [
| "bfs"
| "dfs"
]

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

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

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

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

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

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

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

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" OPT ( "with" bindings )
| "eleft" OPT ( "with" bindings )
| "right" OPT ( "with" bindings )
| "eright" OPT ( "with" bindings )
| "constructor" OPT int_or_var OPT ( "with" bindings )
| "econstructor" OPT ( int_or_var OPT ( "with" bindings ) )
| "specialize" constr_with_bindings OPT ( "as" simple_intropattern )
| "symmetry" OPT ( "in" in_clause )
| "split" OPT ( "with" bindings )
| "esplit" OPT ( "with" bindings )
| "exists" OPT ( LIST1 bindings SEP "," )
| "eexists" OPT ( LIST1 bindings SEP "," )
| "intros" "until" [ ident | num ]
| "intro" OPT ident OPT where
| "move" ident OPT where
| "rename" LIST1 ( ident "into" ident ) SEP ","
| "revert" LIST1 ident
| "simple" "induction" [ ident | num ]
| "simple" "destruct" [ ident | num ]
| "double" "induction" [ ident | num ] [ ident | num ]
| "admit"
| "clear" LIST0 ident
| "clear" "-" LIST1 ident
| "clearbody" LIST1 ident
| "generalize" "dependent" one_term
| "replace" one_term "with" one_term OPT clause_dft_concl OPT ( "by" ltac_expr3 )
| "replace" OPT [ "->" | "<-" ] one_term OPT clause_dft_concl
| "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 OPT ( "using" ident )
| "only" selector ":" ltac_expr3
| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
| "first" "[" LIST0 ltac_expr SEP "|" "]"
| "solve" "[" LIST0 ltac_expr SEP "|" "]"
| "idtac" LIST0 [ ident | string | int ]
| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ]
| "eval" red_expr "in" term
| "context" ident "[" term "]"
| "type" "of" term
| "fresh" LIST0 [ string | qualid ]
| "type_term" one_term
| "numgoals"
| "uconstr" ":" "(" term ")"
| "fun" LIST1 name "=>" ltac_expr
| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
| "info" ltac_expr
| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
| ltac_expr3 ";" "[" for_each_goal "]"
| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
| "[>" for_each_goal "]"
| toplevel_selector ":" ltac_expr
| "simplify_eq" OPT destruction_arg
| "esimplify_eq" OPT destruction_arg
| "discriminate" OPT destruction_arg
| "ediscriminate" OPT destruction_arg
| "injection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
| "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
| "simple" "injection" OPT destruction_arg
| "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
| "decompose" "sum" one_term
| "decompose" "record" one_term
| "absurd" one_term
| "contradiction" OPT constr_with_bindings
| "autorewrite" OPT "*" "with" LIST1 ident OPT clause_dft_concl OPT ( "using" ltac_expr )
| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" occurrences OPT ( "by" ltac_expr3 ) )
| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" occurrences "in" ident OPT ( "by" ltac_expr3 )
| "refine" one_term
| "simple" "refine" one_term
| "notypeclasses" "refine" one_term
| "simple" "notypeclasses" "refine" one_term
| "solve_constraints"
| "subst" OPT ( LIST1 ident )
| "simple" "subst"
| "evar" "(" ident ":" term ")"
| "evar" one_term
| "instantiate" "(" ident ":=" term ")"
| "instantiate" "(" int ":=" term ")" OPT hloc
| "instantiate"
| "stepl" one_term OPT ( "by" ltac_expr )
| "stepr" one_term OPT ( "by" ltac_expr )
| "generalize_eqs" ident
| "dependent" "generalize_eqs" ident
| "generalize_eqs_vars" ident
| "dependent" "generalize_eqs_vars" ident
| "specialize_eqs" ident
| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" int_or_var ) "in" one_term
| "hget_evar" int_or_var
| "destauto" OPT ( "in" ident )
| "transparent_abstract" ltac_expr3 OPT ( "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"
| "with_strategy" strategy_level_or_var "[" LIST1 reference "]" ltac_expr3
| "start" "ltac" "profiling"
| "stop" "ltac" "profiling"
| "reset" "ltac" "profile"
| "show" "ltac" "profile" OPT [ "cutoff" int | string ]
| "restart_timer" OPT string
| "finish_timing" OPT ( "(" string ")" ) OPT string
| "eassumption"
| "eexact" one_term
| "trivial" OPT auto_using OPT hintbases
| "info_trivial" OPT auto_using OPT hintbases
| "debug" "trivial" OPT auto_using OPT hintbases
| "auto" OPT int_or_var OPT auto_using OPT hintbases
| "info_auto" OPT int_or_var OPT auto_using OPT hintbases
| "debug" "auto" OPT int_or_var OPT auto_using OPT hintbases
| "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
| "new" "auto" OPT int_or_var OPT auto_using OPT hintbases
| "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
| "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
| "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases
| "autounfold" OPT hintbases OPT clause_dft_concl
| "autounfold_one" OPT hintbases OPT ( "in" ident )
| "unify" one_term one_term OPT ( "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 OPT ( "in" ident )
| "rewrite_db" ident OPT ( "in" ident )
| "substitute" OPT [ "->" | "<-" ] constr_with_bindings
| "setoid_rewrite" OPT [ "->" | "<-" ] constr_with_bindings OPT ( "at" occurrences ) OPT ( "in" ident )
| "setoid_rewrite" OPT [ "->" | "<-" ] constr_with_bindings "in" ident "at" occurrences
| "setoid_symmetry" OPT ( "in" ident )
| "setoid_reflexivity"
| "setoid_transitivity" one_term
| "setoid_etransitivity"
| "decide" "equality"
| "compare" one_term one_term
| "intros" LIST0 intropattern
| "eintros" LIST0 intropattern
| "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
| "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," OPT 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 OPT ( "with" LIST1 fixdecl )
| "cofix" ident OPT ( "with" LIST1 cofixdecl )
| "pose" bindings_with_parameters
| "pose" one_term OPT as_name
| "epose" bindings_with_parameters
| "epose" one_term OPT as_name
| "set" bindings_with_parameters OPT clause_dft_concl
| "set" one_term OPT as_name OPT clause_dft_concl
| "eset" bindings_with_parameters OPT clause_dft_concl
| "eset" one_term OPT as_name OPT clause_dft_concl
| "remember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all
| "eremember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all
| "assert" "(" ident ":=" term ")"
| "eassert" "(" ident ":=" term ")"
| "assert" "(" ident ":" term ")" OPT ( "by" ltac_expr3 )
| "eassert" "(" ident ":" term ")" OPT ( "by" ltac_expr3 )
| "enough" "(" ident ":" term ")" OPT ( "by" ltac_expr3 )
| "eenough" "(" ident ":" term ")" OPT ( "by" ltac_expr3 )
| "assert" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
| "eassert" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
| "pose" "proof" "(" ident ":=" term ")"
| "epose" "proof" "(" ident ":=" term ")"
| "pose" "proof" term OPT as_ipat
| "epose" "proof" term OPT as_ipat
| "enough" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
| "eenough" one_term OPT as_ipat OPT ( "by" ltac_expr3 )
| "generalize" one_term OPT ( LIST1 one_term )
| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occ OPT as_name ]
| "induction" induction_clause_list
| "einduction" induction_clause_list
| "destruct" induction_clause_list
| "edestruct" induction_clause_list
| "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
| "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | num ] OPT as_or_and_ipat OPT [ "with" one_term ]
| "simple" "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
| "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
| "inversion_clear" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
| "inversion" [ ident | num ] "using" one_term OPT ( "in" LIST1 ident )
| "red" OPT clause_dft_concl
| "hnf" OPT clause_dft_concl
| "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl
| "cbv" OPT strategy_flag OPT clause_dft_concl
| "cbn" OPT strategy_flag OPT clause_dft_concl
| "lazy" OPT strategy_flag OPT clause_dft_concl
| "compute" OPT delta_flag OPT clause_dft_concl
| "vm_compute" OPT ref_or_pattern_occ OPT clause_dft_concl
| "native_compute" OPT ref_or_pattern_occ OPT clause_dft_concl
| "unfold" LIST1 unfold_occ SEP "," OPT clause_dft_concl
| "fold" LIST1 one_term OPT clause_dft_concl
| "pattern" LIST1 pattern_occ SEP "," OPT clause_dft_concl
| "change" conversion OPT clause_dft_concl
| "change_no_check" conversion OPT clause_dft_concl
| "btauto"
| "rtauto"
| "congruence" OPT int OPT ( "with" LIST1 one_term )
| "f_equal"
| "firstorder" OPT ltac_expr firstorder_rhs
| "gintuition" OPT ltac_expr
| "functional" "inversion" [ ident | num ] OPT qualid      (* funind plugin *)
| "functional" "induction" term OPT fun_ind_using OPT with_names      (* funind plugin *)
| "soft" "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
| "psatz_Z" OPT int_or_var ltac_expr
| "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" OPT int_or_var ltac_expr
| "psatz_Q" OPT int_or_var ltac_expr
| "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 OPT ( "in" ident )
| "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 *)
| match_key OPT "reverse" "goal" "with" OPT "|" LIST1 ( goal_pattern "=>" ltac_expr ) SEP "|" "end"
| match_key ltac_expr "with" OPT "|" LIST1 ( match_pattern "=>" ltac_expr ) SEP "|" "end"
| "classical_left"
| "classical_right"
| "contradict" ident
| "discrR"
| "easy"
| "exfalso"
| "inversion_sigma"
| "lia"
| "lra"
| "nia"
| "nra"
| "split_Rabs"
| "split_Rmult"
| "tauto"
| "time_constr" ltac_expr
| "zify"
| "assert_fails" ltac_expr3
| "assert_succeeds" ltac_expr3
| "field" OPT ( "[" LIST1 term "]" )
| "field_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
| "field_simplify_eq" OPT ( "[" LIST1 term "]" ) OPT ( "in" ident )
| "intuition" OPT ltac_expr
| "nsatz" OPT ( "with" "radicalmax" ":=" term "strategy" ":=" term "parameters" ":=" term "variables" ":=" term )
| "psatz" term OPT int_or_var
| "ring" OPT ( "[" LIST1 term "]" )
| "ring_simplify" OPT ( "[" LIST1 term "]" ) LIST1 term OPT ( "in" ident )
| qualid LIST1 tactic_arg
]

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

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
]

as_name: [
| "as" ident
]

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: [
| OPT [ "->" | "<-" ] rewriter
]

induction_clause: [
| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause
]

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

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

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

intropattern_or_list_or: [
| LIST0 intropattern LIST0 ( "|" LIST0 intropattern )
]

equality_intropattern: [
| "->"
| "<-"
| "[=" LIST0 intropattern "]"
]

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_as: [
| "in" ident OPT as_ipat
]

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

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

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

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

constr_with_bindings: [
| one_term OPT ( "with" bindings )
]

destruction_arg: [
| num
| constr_with_bindings
| constr_with_bindings_arg
]

constr_with_bindings_arg: [
| ">" constr_with_bindings
| constr_with_bindings
]

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

with_names: [
| "as" simple_intropattern      (* 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
]

l3_tactic: [
]

l2_tactic: [
]

l1_tactic: [
]

binder_tactic: [
]

value_tactic: [
]

syn_value: [
| ident ":" "(" nonterminal ")"
]

ltac_expr: [
| [ ltac_expr4 | binder_tactic ]
]

ltac_expr4: [
| ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
| ltac_expr3 ";" "[" for_each_goal "]"
| ltac_expr3
]

ltac_expr3: [
| l3_tactic
| ltac_expr2
]

ltac_expr2: [
| ltac_expr1 "+" [ ltac_expr2 | binder_tactic ]
| ltac_expr1 "||" [ ltac_expr2 | binder_tactic ]
| l2_tactic
| ltac_expr1
]

ltac_expr1: [
| tactic_value
| qualid LIST1 tactic_arg
| l1_tactic
| ltac_expr0
]

tactic_value: [
| [ value_tactic | syn_value ]
]

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

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

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

let_clause: [
| name ":=" ltac_expr
| ident LIST1 name ":=" ltac_expr
]

for_each_goal: [
| goal_tactics
| OPT ( goal_tactics "|" ) OPT ltac_expr ".." OPT ( "|" goal_tactics )
]

goal_tactics: [
| LIST0 ( OPT ltac_expr ) SEP "|"
]

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

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

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

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

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

cpattern: [
| term
]

goal_pattern: [
| LIST0 match_hyp SEP "," "|-" match_pattern
| "[" LIST0 match_hyp SEP "," "|-" match_pattern "]"
| "_"
]

match_hyp: [
| name ":" match_pattern
| name ":=" match_pattern
| name ":=" "[" match_pattern "]" ":" match_pattern
]