Quelle  orderedGrammar   Sprache: XML

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

term: [
| term100
]

term100: [
| term_cast
| term10
]

term10: [
| term_application
| term_forall_or_fun
| term_let
| term_fix
| term_cofix
| term_if
| one_term
]

one_term: [
| term_explicit
| term1
]

term1: [
| term_projection
| term_scope
| term0
]

term0: [
| qualid_annotated
| sort
| number_or_string
| term_evar
| term_match
| term_record
| term_generalizing
| "[|" LIST0 term SEP ";" "|" term OPT ( ":" type ) "|]" OPT univ_annot
| term_ltac
| "(" term ")"
]

qualid_annotated: [
| qualid OPT univ_annot
]

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

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

term_scope: [
| term0 "%" scope_key
| 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 ")"
| "(" natural ":=" term ")"
| term1
]

term_explicit: [
| "@" qualid_annotated
]

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

type: [
| term
]

one_type: [
| one_term
]

number: [
| OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
| OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
]

integer: [
| bigint
]

bigint: [
| OPT "-" bignat
]

natural: [
| bignat
]

bignat: [
| [ decnat | hexnat ]
]

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

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

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

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

add_zify: [
| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]      (* Micromega plugin *)
| [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]      (* Micromega plugin *)
]

show_zify: [
| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ]      (* Micromega plugin *)
]

REACHABLE: [
| command
| simple_tactic
| NOTINRSTS
]

NOTINRSTS: [
| command
| control_command
| simple_tactic
| hints_regexp
| REACHABLE
| NOTINRSTS
| l1_tactic
| l3_tactic
| l2_tactic
| value_tactic
| ltac2_entry
| q_intropatterns
| q_intropattern
| q_ident
| q_destruction_arg
| q_with_bindings
| q_bindings
| q_reductions
| q_reference
| q_clause
| q_occurrences
| q_induction_clause
| q_conversion
| q_rewriting
| q_dispatch
| q_hintdb
| q_move_location
| q_pose
| q_assert
| q_constr_matching
| q_goal_matching
]

document: [
| LIST0 sentence
]

nonterminal: [
]

sentence: [
| OPT attributes command "."
| OPT attributes OPT ( natural ":" ) 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
| "=" qualid
| "(" LIST1 attribute SEP "," ")"
]

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

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

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

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

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

univ_annot: [
| "@{" LIST0 univ_level_or_quality OPT [ [ "|" | ";" ] LIST0 univ_level_or_quality ] "}"
]

univ_level_or_quality: [
| "Set"
| "SProp"
| "Prop"
| "Type"
| "_"
| qualid
]

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

cumul_univ_decl: [
| "@{" OPT [ LIST0 ident [ "|" | ";" ] ] LIST0 ( OPT [ "+" | "=" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
]

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

univ_decl_constraints: [
| "|" LIST0 univ_constraint SEP "," [ "+" | ] "}"
| [ "}" | "|}" ]
]

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

fix_decl: [
| 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
| destructuring_let
]

destructuring_let: [
| "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 "," type
| "fun" open_binders "=>" term
]

open_binders: [
| LIST1 name ":" type
| 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 ":>" type
]

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 "%_" scope_key
| pattern0
]

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

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: [
| "lazy" OPT reductions
| "cbv" OPT reductions
| "compute" OPT delta_reductions
| "vm_compute" OPT [ reference_occs | pattern_occs ]
| "native_compute" OPT [ reference_occs | pattern_occs ]
| "red"
| "hnf"
| "simpl" OPT "head" OPT delta_reductions OPT [ reference_occs | pattern_occs ]
| "cbn" OPT reductions
| "unfold" LIST1 reference_occs SEP ","
| "fold" LIST1 one_term
| "pattern" LIST1 pattern_occs SEP ","
| ident
]

reductions: [
| LIST1 reduction
| OPT "head" delta_reductions
]

reduction: [
| "head"
| "beta"
| "delta" OPT delta_reductions
| "match"
| "fix"
| "cofix"
| "iota"
| "zeta"
]

delta_reductions: [
| OPT "-" "[" LIST1 reference "]"
]

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

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

record_definition: [
| OPT ">" ident_decl LIST0 binder OPT [ ":" sort ] OPT ( ":=" OPT ident "{" OPT [ LIST1 record_field SEP ";" OPT ";" ] "}" OPT [ "as" ident ] )
]

record_field: [
| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] name OPT field_spec OPT [ "|" natural ] OPT decl_notations
]

field_spec: [
| LIST0 binder of_type_inst
| LIST0 binder ":=" term
| LIST0 binder of_type_inst ":=" term
]

of_type_inst: [
| [ ":" | ":>" | "::" | "::>" ] type
]

term_record: [
| "{|" OPT [ LIST1 field_val SEP ";" OPT ";" ] "|}"
]

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

inductive_definition: [
| ident OPT cumul_univ_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT [ OPT "|" LIST1 constructor SEP "|" ] OPT decl_notations
]

constructor: [
| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident LIST0 binder OPT of_type_inst
]

import_categories: [
| OPT "-" "(" LIST1 qualid SEP "," ")"
]

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

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

rw_pattern: [
| term
]

rewrite_rule: [
| OPT [ univ_decl "|-" ] rw_pattern "=>" term
]

scheme_kind: [
| scheme_type "for" reference "Sort" sort_quality_or_set
]

scheme_type: [
| "Induction"
| "Minimality"
| "Elimination"
| "Case"
]

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

hint_info: [
| "|" OPT natural OPT one_pattern
]

one_pattern: [
| one_term
]

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

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

functor_app_annot: [
| "[" "inline" "at" "level" natural "]"
| "[" "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
| "(" 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 ]
]

arg_specs: [
| argument_spec
| "/"
| "&"
| "(" LIST1 argument_spec ")" LIST0 [ "%" scope | "%_" scope ]
| "[" LIST1 argument_spec "]" LIST0 [ "%" scope | "%_" scope ]
| "{" LIST1 argument_spec "}" LIST0 [ "%" scope | "%_" scope ]
]

argument_spec: [
| OPT "!" name LIST0 [ "%" scope | "%_" scope ]
]

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

args_modifier: [
| "simpl" "nomatch"
| "simpl" "never"
| "clear" "simpl"
| "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"
| integer
| "expand"
| "transparent"
]

strategy_level_or_var: [
| strategy_level
| ident
]

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

simple_reserv: [
| LIST1 ident ":" type
]

debug_univ_name: [
| qualid
| string
]

command: [
| "Goal" type
| "Pwd"
| "Cd" OPT string
| "Load" OPT "Verbose" [ string | ident ]
| "Declare" "ML" "Module" LIST1 string
| "Locate" reference
| "Locate" "Term" reference
| "Locate" "Module" qualid
| "Info" natural ltac_expr
| "Add" "Zify" add_zify qualid      (* Micromega plugin *)
| "Show" "Zify" show_zify      (* Micromega plugin *)
| "Locate" "Ltac" qualid
| "Locate" "Library" qualid
| "Locate" "File" string
| "Type" term
| "Print" "All"
| "Print" "Section" qualid
| "Print" "Grammar" LIST0 ident
| "Print" "Custom" "Grammar" ident
| "Print" "Keywords"
| "Print" "LoadPath" OPT dirpath
| "Print" "Libraries"
| "Print" "ML" "Path"
| "Print" "ML" "Modules"
| "Print" "Debug" "GC"
| "Print" "Graph"
| "Print" "Classes"
| "Print" "Typeclasses"
| "Print" "Instances" reference
| "Print" "Coercions"
| "Print" "Notation" string OPT [ "in" "custom" ident ]
| "Print" "Coercion" "Paths" coercion_class coercion_class
| "Print" "Canonical" "Projections" LIST0 reference
| "Print" "Typing" "Flags"
| "Print" "Tables"
| "Print" "Options"
| "Print" "Hint" OPT [ "*" | reference ]
| "Print" "HintDb" ident
| "Print" "Scopes"
| "Print" "Scope" scope_name
| "Print" "Visibility" OPT scope_name
| "Print" "Implicit" reference
| "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 debug_univ_name ")" ) OPT [ [ "With" | "Without" ] "Constraint" "Sources" ] OPT string
| "Print" "Sorts"
| "Print" "Assumptions" reference
| "Print" "Opaque" "Dependencies" reference
| "Print" "Transparent" "Dependencies" reference
| "Print" "All" "Dependencies" reference
| "Print" "Strategy" reference
| "Print" "Strategies"
| "Print" "Registered"
| "Print" "Registered" "Schemes"
| "Print" OPT "Term" reference OPT univ_name_list
| "Print" "Module" "Type" qualid
| "Print" "Module" qualid
| "Print" "Namespace" dirpath
| "Inspect" natural
| "Print" "Table" setting_name
| "Add" setting_name LIST1 [ qualid | string ]
| "Test" setting_name OPT ( "for" LIST1 [ qualid | string ] )
| "Remove" setting_name LIST1 [ qualid | string ]
| "Reset" "Initial"
| "Reset" ident
| "Back" OPT natural
| "Debug" [ "On" | "Off" ]
| "Declare" "Reduction" ident ":=" red_expr
| "Declare" "Custom" "Entry" ident
| "Derive" open_binders "SuchThat" type "As" ident
| "Derive" open_binders "in" type "as" ident
| "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 [ ident | integer ] "]"      (* extraction plugin *)
| "Extraction" "Blacklist" LIST1 ident      (* extraction plugin *)
| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
| "Extract" "Callback" OPT string qualid      (* extraction plugin *)
| "Print" "Extraction" "Callback"      (* extraction plugin *)
| "Reset" "Extraction" "Callback"      (* extraction plugin *)
| "Print" "Extraction" "Foreign"      (* extraction plugin *)
| "Extract" "Constant" qualid LIST0 string "=>" [ ident | string ]      (* extraction plugin *)
| "Extract" "Foreign" "Constant" qualid "=>" 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 *)
| "Proof"
| "Proof" "Mode" string
| "Proof" term
| "Abort" OPT "All"
| "Admitted"
| "Qed"
| "Save" ident
| "Defined" OPT ident
| "Restart"
| "Undo" OPT ( OPT "To" natural )
| "Focus" OPT natural
| "Unfocus"
| "Unfocused"
| "Show" OPT [ ident | natural ]
| "Show" "Existentials"
| "Show" "Universes"
| "Show" "Conjectures"
| "Show" "Proof" OPT ( "Diffs" OPT "removed" )
| "Show" "Intro"
| "Show" "Intros"
| "Show" "Match" qualid
| "Guarded"
| "Validate" "Proof"
| "Create" "HintDb" ident OPT "discriminated"
| "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
| "Comments" LIST0 [ one_term | string | natural ]
| "Attributes" LIST1 attribute SEP ","
| "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
| "Declare" "Scope" scope_name
| "Obligation" natural OPT ( "of" ident ) OPT ( "with" generic_tactic )
| "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" generic_tactic )
| "Final" "Obligation" OPT ( "of" ident ) OPT ( "with" generic_tactic )
| "Solve" "Obligations" OPT ( "of" ident ) OPT ( "with" ltac_expr )
| "Solve" "All" "Obligations" OPT ( "with" ltac_expr )
| "Admit" "Obligations" OPT ( "of" ident )
| "Obligation" "Tactic" ":=" generic_tactic
| "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
| "Unshelve"
| "Declare" "Equivalent" "Keys" one_term one_term
| "Print" "Equivalent" "Keys"
| "Optimize" "Proof"
| "Optimize" "Heap"
| "infoH" ltac_expr
| "Reset" "Ltac" "Profile"
| "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
| "Show" "Lia" "Profile"      (* micromega plugin *)
| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* ring plugin *)
| "Print" "Rings"      (* ring plugin *)
| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
| "Print" "Fields"      (* ring plugin *)
| "Hint" "Cut" "[" hints_regexp "]" OPT ( ":" LIST1 ident )
| "Typeclasses" "Transparent" LIST1 qualid
| "Typeclasses" "Opaque" LIST1 qualid
| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
| "Proof" "with" generic_tactic OPT [ "using" section_var_expr ]
| "Proof" "using" section_var_expr OPT [ "with" generic_tactic ]
| "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
| "Print" "Rewrite" "HintDb" ident
| "Print" "Ltac" qualid
| "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
| "Print" "Ltac" "Signatures"
| "Print" "Firstorder" "Solver"
| "Function" fix_definition LIST0 ( "with" fix_definition )
| "Functional" "Scheme" func_scheme_def LIST0 ( "with" func_scheme_def )
| "Functional" "Case" func_scheme_def      (* funind plugin *)
| "Generate" "graph" "for" qualid      (* funind plugin *)
| "Hint" "Rewrite" OPT [ "->" | "<-" ] LIST1 one_term OPT ( "using" generic_tactic ) OPT ( ":" LIST1 ident )
| "Derive" "Inversion_clear" ident "with" one_term OPT ( "Sort" sort_quality_or_set )
| "Derive" "Inversion" ident "with" one_term OPT ( "Sort" sort_quality_or_set )
| "Derive" "Dependent" "Inversion" ident "with" one_term "Sort" sort_quality_or_set
| "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_quality_or_set
| "Declare" "Left" "Step" one_term
| "Declare" "Right" "Step" one_term
| "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name
| "String" "Notation" qualid qualid qualid OPT ( "(" number_string_via ")" ) ":" 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 ( "(" natural ")" ) ) [ assumpt | LIST1 ( "(" assumpt ")" ) ]
| [ "Definition" | "Example" ] ident_decl def_body
| [ "Symbol" | "Symbols" ] [ assumpt | LIST1 ( "(" assumpt ")" ) ]
| "Let" ident_decl def_body
| "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
| "Inductive" record_definition LIST0 ( "with" record_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 )
| "Scheme" OPT "Boolean" "Equality" "for" reference
| "Combined" "Scheme" ident "from" LIST1 ident SEP ","
| "Register" qualid "as" qualid
| "Register" "Scheme" qualid "as" qualid "for" qualid
| "Register" "Inline" qualid
| "Primitive" ident_decl OPT [ ":" term ] ":=" "#" ident
| "Universe" LIST1 ident
| "Universes" LIST1 ident
| "Sort" LIST1 ident
| "Sorts" LIST1 ident
| "Constraint" LIST1 univ_constraint SEP ","
| "Rewrite" [ "Rule" | "Rules" ] ident ":=" OPT "|" LIST1 rewrite_rule SEP "|"
| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
| "CoInductive" record_definition LIST0 ( "with" record_definition )
| "Variant" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT [ OPT "|" LIST1 constructor SEP "|" ] OPT decl_notations
| [ "Record" | "Structure" ] record_definition
| "Class" record_definition
| "Class" ident_decl LIST0 binder OPT [ ":" sort ] ":=" constructor
| "Module" OPT ( [ "Import" | "Export" ] OPT import_categories ) 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" ] OPT import_categories ) ident LIST0 module_binder ":" module_type_inl
| "Section" ident
| "End" ident
| "Collection" ident ":=" section_var_expr
| "From" dirpath "Extra" "Dependency" string OPT [ "as" ident ]
| OPT [ "From" dirpath ] "Require" OPT ( [ "Import" | "Export" ] OPT import_categories ) LIST1 filtered_import
| "Import" OPT import_categories LIST1 filtered_import
| "Export" OPT import_categories LIST1 filtered_import
| "Include" module_type_inl LIST0 ( "<+" module_type_inl )
| "Include" "Type" LIST1 module_type_inl SEP "<+"
| "Transparent" OPT "!" LIST1 reference
| "Opaque" OPT "!" LIST1 reference
| "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ]
| "Canonical" OPT "Structure" ident_decl def_body
| "Canonical" OPT "Structure" reference
| "Coercion" ident_decl def_body
| "Identity" "Coercion" ident ":" coercion_class ">->" coercion_class
| "Coercion" reference OPT [ ":" coercion_class ">->" coercion_class ]
| "Context" LIST1 binder
| "Instance" OPT ( ident_decl LIST0 binder ) ":" type OPT hint_info OPT [ ":=" "{" LIST0 field_val "}" | ":=" term ]
| "Existing" "Instance" qualid OPT hint_info
| "Existing" "Instances" LIST1 qualid OPT [ "|" natural ]
| "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 [ integer | 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 coercion_class
| "Infix" notation_declaration
| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
| "Notation" notation_declaration
| "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
| "Reserved" "Notation" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
| [ "Enable" | "Disable" ] "Notation" OPT [ string | qualid LIST0 ident ] OPT ( ":=" one_term ) OPT ( "(" LIST1 enable_notation_flag SEP "," ")" ) OPT [ ":" scope_name | ":" "no" "scope" ]
| "Eval" red_expr "in" term
| "Compute" term
| "Check" term
| "About" reference OPT univ_name_list
| "SearchPattern" one_pattern OPT ( [ "inside" | "in" | "outside" ] LIST1 qualid )
| "SearchRewrite" one_pattern OPT ( [ "inside" | "in" | "outside" ] LIST1 qualid )
| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "in" | "outside" ] LIST1 qualid )
| "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
| "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
| "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string
| "Ltac2" "Notation" LIST1 ltac2_syntax_class OPT ( ":" natural ) ":=" ltac2_expr      (* ltac2 plugin *)
| "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr
| "Ltac2" "Notation" ident ":=" ltac2_expr      (* Ltac2 plugin *)
| "Ltac2" "Eval" ltac2_expr      (* ltac2 plugin *)
| "Print" "Ltac2" qualid      (* ltac2 plugin *)
| "Print" "Ltac2" "Type" qualid      (* ltac2 plugin *)
| "Locate" "Ltac2" qualid      (* ltac2 plugin *)
| "Print" "Ltac2" "Signatures"      (* ltac2 plugin *)
| "Ltac2" "Check" ltac2_expr      (* ltac2 plugin *)
| "Ltac2" "Globalize" ltac2_expr      (* ltac2 plugin *)
| "Hint" "Resolve" LIST1 [ qualid | one_term ] OPT hint_info OPT ( ":" LIST1 ident )
| "Hint" "Resolve" [ "->" | "<-" ] LIST1 qualid OPT natural OPT ( ":" LIST1 ident )
| "Hint" "Immediate" LIST1 [ qualid | one_term ] OPT ( ":" LIST1 ident )
| "Hint" [ "Constants" | "Projections" | "Variables" ] [ "Transparent" | "Opaque" ] OPT ( ":" LIST1 ident )
| "Hint" [ "Transparent" | "Opaque" ] LIST1 qualid OPT ( ":" LIST1 ident )
| "Hint" "Mode" qualid LIST1 [ "+" | "!" | "-" ] OPT ( ":" LIST1 ident )
| "Hint" "Unfold" LIST1 qualid OPT ( ":" LIST1 ident )
| "Hint" "Constructors" LIST1 qualid OPT ( ":" LIST1 ident )
| "Hint" "Extern" natural OPT one_pattern "=>" generic_tactic OPT ( ":" LIST1 ident )
| "Time" sentence
| "Instructions" sentence
| "Profile" OPT string sentence
| "Redirect" string sentence
| "Timeout" natural sentence
| "Fail" sentence
| "Succeed" sentence
| "Drop"
| "Quit"
| "BackTo" natural
| "Show" "Goal" natural "at" natural
]

section_var_expr: [
| LIST0 starred_ident_ref
| OPT "-" section_var_expr50
]

section_var_expr50: [
| section_var_expr0 "-" section_var_expr0
| section_var_expr0 "+" section_var_expr0
| section_var_expr0
]

section_var_expr0: [
| starred_ident_ref
| "()"
| "(" section_var_expr ")" OPT "*"
]

starred_ident_ref: [
| ident OPT "*"
| "Type" OPT "*"
| "All"
]

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_pattern
| "is" ":" logical_kind
]

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

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

enable_notation_flag: [
| "all"
| "only" "parsing"
| "only" "printing"
| "in" "custom" ident
| "in" "constr"
]

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

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

ltac2_type: [
| ltac2_type2 "->" ltac2_type      (* ltac2 plugin *)
| ltac2_type2      (* ltac2 plugin *)
]

ltac2_type2: [
| ltac2_type1 "*" LIST1 ltac2_type1 SEP "*"      (* ltac2 plugin *)
| ltac2_type1      (* ltac2 plugin *)
]

ltac2_type1: [
| ltac2_type0 qualid      (* ltac2 plugin *)
| ltac2_type0      (* ltac2 plugin *)
]

ltac2_type0: [
| "(" LIST1 ltac2_type SEP "," ")" OPT qualid      (* ltac2 plugin *)
| ltac2_typevar      (* ltac2 plugin *)
| "_"      (* ltac2 plugin *)
| qualid      (* ltac2 plugin *)
]

ltac2_typevar: [
| "'" ident      (* ltac2 plugin *)
]

occurrences: [
| "at" occs_nums
| "in" goal_occurrences
]

simple_occurrences: [
| occurrences
]

occs_nums: [
| OPT "-" LIST1 nat_or_var
]

nat_or_var: [
| [ natural | ident ]
]

goal_occurrences: [
| LIST1 hyp_occs SEP "," OPT ( "|-" OPT concl_occs )
| "*" "|-" OPT concl_occs
| "|-" OPT concl_occs
| OPT concl_occs
]

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

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

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

q_intropatterns: [
| ltac2_intropatterns      (* ltac2 plugin *)
]

ltac2_intropatterns: [
| LIST0 nonsimple_intropattern      (* ltac2 plugin *)
]

nonsimple_intropattern: [
| "*"      (* ltac2 plugin *)
| "**"      (* ltac2 plugin *)
| ltac2_simple_intropattern      (* ltac2 plugin *)
]

q_intropattern: [
| ltac2_simple_intropattern      (* ltac2 plugin *)
]

ltac2_simple_intropattern: [
| ltac2_simple_intropattern_closed LIST0 [ "%" term0 ]      (* ltac2 plugin *)
]

ltac2_simple_intropattern_closed: [
| ltac2_or_and_intropattern      (* ltac2 plugin *)
| ltac2_equality_intropattern      (* ltac2 plugin *)
| "_"      (* ltac2 plugin *)
| ltac2_naming_intropattern      (* ltac2 plugin *)
]

ltac2_naming_intropattern: [
| "?" ident      (* ltac2 plugin *)
| "?$" ident      (* ltac2 plugin *)
| "?"      (* ltac2 plugin *)
| ident_or_anti      (* ltac2 plugin *)
]

ltac2_or_and_intropattern: [
| "[" LIST1 ltac2_intropatterns SEP "|" "]"      (* ltac2 plugin *)
| "()"      (* ltac2 plugin *)
| "(" LIST1 ltac2_simple_intropattern SEP "," ")"      (* Ltac2 plugin *)
| "(" LIST1 ltac2_simple_intropattern SEP "&" ")"      (* Ltac2 plugin *)
]

ltac2_equality_intropattern: [
| "->"      (* ltac2 plugin *)
| "<-"      (* ltac2 plugin *)
| "[=" ltac2_intropatterns "]"
]

q_ident: [
| ident_or_anti      (* ltac2 plugin *)
]

ident_or_anti: [
| ident
| "$" ident      (* ltac2 plugin *)
]

q_destruction_arg: [
| ltac2_destruction_arg      (* ltac2 plugin *)
]

ltac2_destruction_arg: [
| natural      (* ltac2 plugin *)
| ident
| ltac2_constr_with_bindings      (* ltac2 plugin *)
]

ltac2_constr_with_bindings: [
| term OPT ( "with" ltac2_bindings )      (* ltac2 plugin *)
]

q_bindings: [
| ltac2_bindings      (* ltac2 plugin *)
]

q_with_bindings: [
| OPT ( "with" ltac2_bindings )      (* ltac2 plugin *)
]

ltac2_bindings: [
| LIST1 ltac2_simple_binding      (* ltac2 plugin *)
| LIST1 term      (* ltac2 plugin *)
]

ltac2_simple_binding: [
| "(" qhyp ":=" term ")"      (* ltac2 plugin *)
]

qhyp: [
| "$" ident      (* ltac2 plugin *)
| natural      (* ltac2 plugin *)
| ident
]

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

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

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

number_modifier: [
| "warning" "after" bignat
| "abstract" "after" bignat
| number_string_via
]

number_string_via: [
| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]"
]

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

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

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

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

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

level: [
| "level" natural
| "next" "level"
]

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

notation_declaration: [
| string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
]

simple_tactic: [
| "reflexivity"
| "exact" one_term
| "assumption"
| "etransitivity"
| "cut" one_type
| "exact_no_check" one_term
| "vm_cast_no_check" one_term
| "native_cast_no_check" 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 nat_or_var OPT ( "with" bindings )
| "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) )
| "specialize" one_term_with_bindings OPT as_ipat
| "symmetry" OPT simple_occurrences
| "split" OPT ( "with" bindings )
| "esplit" OPT ( "with" bindings )
| "exists" LIST0 bindings SEP ","
| "eexists" LIST0 bindings SEP ","
| "intros" "until" [ ident | natural ]
| "intro" OPT ident OPT where
| "move" ident where
| "rename" LIST1 ( ident "into" ident ) SEP ","
| "revert" LIST1 ident
| "simple" "induction" [ ident | natural ]
| "simple" "destruct" [ ident | natural ]
| "admit"
| "clear" OPT ( OPT "-" LIST1 ident )
| "clearbody" LIST1 ident
| "simplify_eq" OPT induction_arg
| "esimplify_eq" OPT induction_arg
| "discriminate" OPT induction_arg
| "ediscriminate" OPT induction_arg
| "injection" OPT induction_arg OPT ( "as" LIST0 simple_intropattern )
| "einjection" OPT induction_arg OPT ( "as" LIST0 simple_intropattern )
| "simple" "injection" OPT induction_arg
| "replace" OPT [ "->" | "<-" ] one_term OPT occurrences
| "replace" OPT [ "->" | "<-" ] one_term "with" one_term OPT occurrences OPT ( "by" ltac_expr3 )
| "typeclasses" "eauto" OPT [ "bfs" | "dfs" | "best_effort" ] OPT nat_or_var OPT ( "with" LIST1 ident )
| "setoid_replace" one_term "with" one_term OPT ( "using" "relation" one_term ) OPT ( "in" ident ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 )
| OPT ( [ natural | "[" ident "]" ] ":" ) "{"
| [ LIST1 "-" | LIST1 "+" | LIST1 "*" ]
| "}"
| "try" ltac_expr3
| "do" nat_or_var ltac_expr3
| "timeout" nat_or_var ltac_expr3
| "time" OPT string ltac_expr3
| "repeat" ltac_expr3
| "progress" ltac_expr3
| "once" ltac_expr3
| "exactly_once" ltac_expr3
| "abstract" ltac_expr2 OPT ( "using" ident )
| "only" goal_selector ":" ltac_expr3
| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
| "first" "[" LIST0 ltac_expr SEP "|" "]"
| "first" ident
| "solve" "[" LIST0 ltac_expr SEP "|" "]"
| "solve" ident
| "idtac" LIST0 [ ident | string | natural ]
| [ "fail" | "gfail" ] OPT nat_or_var LIST0 [ ident | string | natural ]
| "eval" red_expr "in" term
| "context" ident "[" term "]"
| "type" "of" term
| "fresh" LIST0 [ string | qualid ]
| "type_term" one_term
| "numgoals"
| "fun" LIST1 name "=>" ltac_expr
| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr
| ltac_expr3 ";" ltac_expr3
| ltac_expr3 ";" "[" for_each_goal "]"
| ltac_expr1 "+" ltac_expr2
| ltac_expr1 "||" ltac_expr2
| "[>" for_each_goal "]"
| toplevel_selector ":" ltac_expr
| ltac2_match_key ltac2_expr "with" ltac2_match_list "end"
| ltac2_match_key OPT "reverse" "goal" "with" goal_match_list "end"
| "case_eq" one_term
| "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
| "decompose" "sum" one_term
| "decompose" "record" one_term
| "absurd" one_type
| "contradiction" OPT one_term_with_bindings
| "autorewrite" OPT "*" "with" LIST1 ident OPT occurrences OPT ( "using" ltac_expr )
| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs ) OPT ( "by" ltac_expr3 )
| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" rewrite_occs "in" ident OPT ( "by" ltac_expr3 )
| OPT "simple" OPT "notypeclasses" "refine" one_term
| "solve_constraints"
| "subst" LIST0 ident
| "simple" "subst"
| "evar" "(" ident ":" type ")"
| "evar" one_type
| "instantiate" "(" ident ":=" term ")"
| "instantiate" "(" natural ":=" term ")" OPT hloc
| "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
| "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" integer | 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 nat_or_var OPT auto_using OPT hintbases
| "info_auto" OPT nat_or_var OPT auto_using OPT hintbases
| "debug" "auto" OPT nat_or_var OPT auto_using OPT hintbases
| "eauto" OPT nat_or_var OPT auto_using OPT hintbases
| "debug" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
| "info_eauto" OPT nat_or_var OPT auto_using OPT hintbases
| "autounfold" OPT hintbases OPT simple_occurrences
| "autounfold_one" OPT hintbases OPT ( "in" ident )
| "unify" one_term one_term OPT ( "with" ident )
| "convert" one_term one_term
| "head_of_constr" ident one_term
| "not_evar" one_term
| "is_ground" one_term
| "autoapply" one_term "with" ident
| "rewrite_strat" rewstrategy OPT ( "in" ident )
| "rewrite_db" ident OPT ( "in" ident )
| "substitute" OPT [ "->" | "<-" ] one_term_with_bindings
| "setoid_rewrite" OPT [ "->" | "<-" ] one_term_with_bindings OPT ( "at" rewrite_occs ) OPT ( "in" ident )
| "setoid_rewrite" OPT [ "->" | "<-" ] one_term_with_bindings "in" ident "at" rewrite_occs
| "setoid_symmetry" OPT ( "in" ident )
| "setoid_reflexivity"
| "setoid_transitivity" one_term
| "setoid_etransitivity"
| "intros" LIST0 intropattern
| "eintros" LIST0 intropattern
| "decide" "equality"
| "compare" one_term one_term
| "apply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as
| "eapply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as
| "simple" "apply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as
| "simple" "eapply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as
| "elim" one_term_with_bindings OPT ( "using" one_term_with_bindings )
| "eelim" one_term_with_bindings OPT ( "using" one_term_with_bindings )
| "case" LIST1 induction_clause SEP "," OPT induction_principle
| "ecase" LIST1 induction_clause SEP "," OPT induction_principle
| "fix" ident natural OPT ( "with" LIST1 ( "(" ident LIST0 simple_binder OPT ( "{" "struct" name "}" ) ":" type ")" ) )
| "cofix" ident OPT ( "with" LIST1 ( "(" ident LIST0 simple_binder ":" type ")" ) )
| "pose" alias_definition
| "pose" one_term OPT as_name
| "epose" alias_definition
| "epose" one_term OPT as_name
| "pose" "proof" "(" ident ":=" term ")"
| "pose" "proof" term OPT as_ipat
| "epose" "proof" "(" ident ":=" term ")"
| "epose" "proof" term OPT as_ipat
| "set" alias_definition OPT occurrences
| "set" one_term OPT as_name OPT occurrences
| "eset" alias_definition OPT occurrences
| "eset" one_term OPT as_name OPT occurrences
| "remember" one_term OPT as_name OPT ( "eqn" ":" naming_intropattern ) OPT ( "in" goal_occurrences )
| "eremember" one_term OPT as_name OPT ( "eqn" ":" naming_intropattern ) OPT ( "in" goal_occurrences )
| "assert" "(" ident ":" type ")" OPT ( "by" ltac_expr3 )
| "assert" "(" ident ":=" term ")"
| "assert" one_type OPT as_ipat OPT ( "by" ltac_expr3 )
| "eassert" "(" ident ":" type ")" OPT ( "by" ltac_expr3 )
| "eassert" "(" ident ":=" term ")"
| "eassert" one_type OPT as_ipat OPT ( "by" ltac_expr3 )
| "enough" "(" ident ":" type ")" OPT ( "by" ltac_expr3 )
| "eenough" "(" ident ":" type ")" OPT ( "by" ltac_expr3 )
| "enough" one_type OPT as_ipat OPT ( "by" ltac_expr3 )
| "eenough" one_type OPT as_ipat OPT ( "by" ltac_expr3 )
| "generalize" "dependent" one_term
| "generalize" LIST1 one_term
| "generalize" LIST1 [ pattern_occs OPT as_name ] SEP ","
| "induction" LIST1 induction_clause SEP "," OPT induction_principle
| "einduction" LIST1 induction_clause SEP "," OPT induction_principle
| "destruct" LIST1 induction_clause SEP "," OPT induction_principle
| "edestruct" LIST1 induction_clause SEP "," OPT induction_principle
| "rewrite" LIST1 oriented_rewriter SEP "," OPT occurrences OPT ( "by" ltac_expr3 )
| "erewrite" LIST1 oriented_rewriter SEP "," OPT occurrences OPT ( "by" ltac_expr3 )
| "simple" "inversion" [ ident | natural ] OPT ( "as" or_and_intropattern ) OPT ( "in" LIST1 ident )
| "inversion" [ ident | natural ] OPT ( "as" or_and_intropattern ) OPT ( "in" LIST1 ident )
| "inversion_clear" [ ident | natural ] OPT ( "as" or_and_intropattern ) OPT ( "in" LIST1 ident )
| "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident )
| "red" simple_occurrences
| "hnf" simple_occurrences
| "simpl" OPT "head" OPT delta_reductions OPT [ reference_occs | pattern_occs ] simple_occurrences
| "cbv" OPT reductions simple_occurrences
| "cbn" OPT reductions simple_occurrences
| "lazy" OPT reductions simple_occurrences
| "compute" OPT delta_reductions simple_occurrences
| "vm_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences
| "native_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences
| "unfold" LIST1 reference_occs SEP "," OPT occurrences
| "fold" LIST1 one_term simple_occurrences
| "pattern" LIST1 pattern_occs SEP "," OPT occurrences
| "change" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences
| "change_no_check" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences
| "btauto"
| "rtauto"
| "congruence" OPT natural OPT ( "with" LIST1 one_term )
| "simple" "congruence" OPT natural OPT ( "with" LIST1 one_term )
| "f_equal"
| "firstorder" OPT ltac_expr OPT ( "using" LIST1 qualid SEP "," ) OPT ( "with" LIST1 ident )
| "functional" "inversion" [ ident | natural ] OPT qualid      (* funind plugin *)
| "functional" "induction" term OPT ( "using" one_term_with_bindings ) OPT ( "as" simple_intropattern )      (* funind plugin *)
| "soft" "functional" "induction" LIST1 one_term OPT ( "using" one_term_with_bindings ) OPT ( "as" simple_intropattern )      (* funind plugin *)
| "xlra_Q" ltac_expr      (* micromega plugin *)
| "wlra_Q" ident one_term      (* micromega plugin *)
| "xlra_R" ltac_expr      (* micromega plugin *)
| "xlia" ltac_expr      (* micromega plugin *)
| "wlia" ident one_term      (* micromega plugin *)
| "xnra_Q" ltac_expr      (* micromega plugin *)
| "wnra_Q" ident one_term      (* micromega plugin *)
| "xnra_R" ltac_expr      (* micromega plugin *)
| "xnia" ltac_expr      (* micromega plugin *)
| "wnia" ident one_term      (* micromega plugin *)
| "xsos_Z" ltac_expr      (* micromega plugin *)
| "wsos_Z" ident one_term      (* micromega plugin *)
| "xsos_Q" ltac_expr      (* micromega plugin *)
| "wsos_Q" ident one_term      (* micromega plugin *)
| "xsos_R" ltac_expr      (* micromega plugin *)
| "xpsatz_Z" nat_or_var ltac_expr      (* micromega plugin *)
| "wpsatz_Z" nat_or_var ident one_term      (* micromega plugin *)
| "xpsatz_Q" nat_or_var ltac_expr      (* micromega plugin *)
| "wpsatz_Q" nat_or_var ident one_term      (* micromega plugin *)
| "xpsatz_R" nat_or_var ltac_expr      (* micromega plugin *)
| "zify_iter_specs"      (* micromega plugin *)
| "zify_op"      (* micromega plugin *)
| "zify_saturate"      (* micromega plugin *)
| "zify_iter_let" ltac_expr      (* micromega plugin *)
| "zify_elim_let"      (* micromega plugin *)
| "nsatz_compute" one_term      (* nsatz plugin *)
| "protect_fv" string OPT ( "in" ident )
| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* 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"
| "dependent" "inversion" [ ident | natural ] OPT ( "as" or_and_intropattern ) OPT [ "with" one_term ]
| "dependent" "simple" "inversion" [ ident | natural ] OPT ( "as" or_and_intropattern ) OPT [ "with" one_term ]
| "dependent" "inversion_clear" [ ident | natural ] OPT ( "as" or_and_intropattern ) OPT [ "with" one_term ]
| "classical_left"
| "classical_right"
| "contradict" ident
| "dintuition" OPT ltac_expr
| "dtauto"
| "easy"
| "exfalso"
| "inversion_sigma" OPT ( ident OPT ( "as" simple_intropattern ) )
| "lia"
| "lra"
| "nia"
| "now_show" one_type
| "nra"
| "rapply" one_term
| "tauto"
| "time_constr" ltac_expr
| "zify"
| "assert_fails" ltac_expr3
| "assert_succeeds" ltac_expr3
| "clear" "dependent" ident
| "decide" one_term "with" one_term
| "dependent" "destruction" ident OPT ( "generalizing" LIST1 ident ) OPT ( "using" one_term )
| "dependent" "induction" ident OPT ( [ "generalizing" | "in" ] LIST1 ident ) OPT ( "using" one_term )
| "field" OPT ( "[" LIST1 one_term "]" )
| "field_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
| "field_simplify_eq" OPT ( "[" LIST1 one_term "]" ) OPT ( "in" ident )
| "intuition" OPT ltac_expr
| "now" ltac_expr
| "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term )
| "psatz" one_term OPT nat_or_var
| "revert" "dependent" ident
| "ring" OPT ( "[" LIST1 one_term "]" )
| "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
| "match" ltac2_expr5 "with" OPT ltac2_branches "end"
| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5
| qualid LIST1 tactic_arg
]

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

in_hyp_as: [
| "in" LIST1 [ ident OPT as_ipat ] SEP ","
]

as_ipat: [
| "as" simple_intropattern
]

oriented_rewriter: [
| OPT [ "->" | "<-" ] OPT natural OPT [ "?" | "!" ] one_term_with_bindings
]

induction_clause: [
| induction_arg OPT ( "as" or_and_intropattern ) OPT ( "eqn" ":" naming_intropattern ) OPT occurrences
]

induction_arg: [
| one_term_with_bindings
| natural
]

induction_principle: [
| "using" one_term_with_bindings OPT occurrences
]

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

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

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

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

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

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

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

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

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

bindings: [
| LIST1 one_term
| LIST1 ( "(" [ ident | natural ] ":=" term ")" )
]

int_or_var: [
| [ integer | ident ]
]

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

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

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

as_name: [
| "as" ident
]

q_clause: [
| ltac2_clause      (* Ltac2 plugin *)
]

ltac2_clause: [
| "in" ltac2_in_clause      (* ltac2 plugin *)
| "at" ltac2_occs_nums      (* ltac2 plugin *)
]

ltac2_in_clause: [
| "*" OPT ltac2_occs      (* ltac2 plugin *)
| "*" "|-" OPT ltac2_concl_occ      (* ltac2 plugin *)
| LIST0 ltac2_hypident_occ SEP "," OPT ( "|-" OPT ltac2_concl_occ )      (* Ltac2 plugin *)
]

q_occurrences: [
| OPT ltac2_occs      (* ltac2 plugin *)
]

ltac2_occs: [
| "at" ltac2_occs_nums      (* ltac2 plugin *)
]

ltac2_occs_nums: [
| OPT "-" LIST1 [ natural | "$" ident ]      (* Ltac2 plugin *)
]

ltac2_concl_occ: [
| "*" OPT ltac2_occs      (* ltac2 plugin *)
]

ltac2_hypident_occ: [
| ltac2_hypident OPT ltac2_occs      (* ltac2 plugin *)
]

ltac2_hypident: [
| ident_or_anti      (* ltac2 plugin *)
| "(" "type" "of" ident_or_anti ")"      (* ltac2 plugin *)
| "(" "value" "of" ident_or_anti ")"      (* ltac2 plugin *)
]

q_induction_clause: [
| ltac2_induction_clause      (* ltac2 plugin *)
]

ltac2_induction_clause: [
| ltac2_destruction_arg OPT ltac2_as_or_and_ipat OPT ltac2_eqn_ipat OPT ltac2_clause      (* Ltac2 plugin *)
]

ltac2_as_or_and_ipat: [
| "as" ltac2_or_and_intropattern      (* ltac2 plugin *)
]

ltac2_eqn_ipat: [
| "eqn" ":" ltac2_naming_intropattern      (* ltac2 plugin *)
]

q_conversion: [
| ltac2_conversion      (* ltac2 plugin *)
]

ltac2_conversion: [
| term      (* ltac2 plugin *)
| term "with" term      (* ltac2 plugin *)
]

q_rewriting: [
| ltac2_oriented_rewriter      (* ltac2 plugin *)
]

ltac2_oriented_rewriter: [
| OPT q_orient ltac2_rewriter      (* ltac2 plugin *)
]

q_orient: [
| OPT [ "->" | "<-" ]
]

ltac2_rewriter: [
| OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings
]

q_dispatch: [
| ltac2_for_each_goal      (* ltac2 plugin *)
]

ltac2_for_each_goal: [
| ltac2_goal_tactics      (* Ltac2 plugin *)
| OPT ( ltac2_goal_tactics "|" ) OPT ltac2_expr ".." OPT ( "|" ltac2_goal_tactics )      (* Ltac2 plugin *)
]

ltac2_goal_tactics: [
| LIST0 ( OPT ltac2_expr ) SEP "|"      (* Ltac2 plugin *)
]

q_reductions: [
| ltac2_reductions      (* ltac2 plugin *)
]

ltac2_reductions: [
| LIST1 ltac2_red_flag      (* ltac2 plugin *)
| OPT ltac2_delta_reductions      (* ltac2 plugin *)
]

ltac2_red_flag: [
| "beta"      (* ltac2 plugin *)
| "iota"      (* ltac2 plugin *)
| "match"      (* ltac2 plugin *)
| "fix"      (* ltac2 plugin *)
| "cofix"      (* ltac2 plugin *)
| "zeta"      (* ltac2 plugin *)
| "delta" OPT ltac2_delta_reductions      (* ltac2 plugin *)
| "head"      (* ltac2 plugin *)
]

ltac2_delta_reductions: [
| OPT "-" "[" LIST1 refglobal "]"
]

q_reference: [
| refglobal      (* ltac2 plugin *)
]

refglobal: [
| "&" ident      (* ltac2 plugin *)
| qualid      (* ltac2 plugin *)
| "$" ident      (* ltac2 plugin *)
]

q_hintdb: [
| hintdb      (* ltac2 plugin *)
]

hintdb: [
| "*"      (* ltac2 plugin *)
| LIST1 ident_or_anti      (* ltac2 plugin *)
]

q_constr_matching: [
| ltac2_match_list      (* ltac2 plugin *)
]

ltac2_match_key: [
| "lazy_match!"
| "match!"
| "multi_match!"
]

ltac2_match_list: [
| OPT "|" LIST1 ltac2_match_rule SEP "|"
]

ltac2_match_rule: [
| ltac2_match_pattern "=>" ltac2_expr      (* ltac2 plugin *)
]

ltac2_match_pattern: [
| cpattern      (* ltac2 plugin *)
| "context" OPT ident "[" cpattern "]"      (* ltac2 plugin *)
]

q_goal_matching: [
| goal_match_list      (* ltac2 plugin *)
]

goal_match_list: [
| OPT "|" LIST1 gmatch_rule SEP "|"
]

gmatch_rule: [
| gmatch_pattern "=>" ltac2_expr      (* ltac2 plugin *)
]

gmatch_pattern: [
| "[" LIST0 gmatch_hyp_pattern SEP "," "|-" ltac2_match_pattern "]"      (* ltac2 plugin *)
]

gmatch_hyp_pattern: [
| name ":" ltac2_match_pattern      (* ltac2 plugin *)
| name ":=" "[" ltac2_match_pattern "]" ":" ltac2_match_pattern      (* ltac2 plugin *)
| name ":=" ltac2_match_pattern      (* ltac2 plugin *)
]

q_move_location: [
| move_location      (* ltac2 plugin *)
]

move_location: [
| "at" "top"      (* ltac2 plugin *)
| "at" "bottom"      (* ltac2 plugin *)
| "after" ident_or_anti      (* ltac2 plugin *)
| "before" ident_or_anti      (* ltac2 plugin *)
]

q_pose: [
| pose      (* ltac2 plugin *)
]

pose: [
| "(" ident_or_anti ":=" term ")"      (* ltac2 plugin *)
| term OPT ltac2_as_name      (* ltac2 plugin *)
]

ltac2_as_name: [
| "as" ident_or_anti      (* ltac2 plugin *)
]

q_assert: [
| assertion      (* ltac2 plugin *)
]

assertion: [
| "(" ident_or_anti ":=" term ")"      (* ltac2 plugin *)
| "(" ident_or_anti ":" term ")" OPT ltac2_by_tactic      (* ltac2 plugin *)
| term OPT ltac2_as_ipat OPT ltac2_by_tactic      (* ltac2 plugin *)
]

ltac2_as_ipat: [
| "as" ltac2_simple_intropattern      (* ltac2 plugin *)
]

ltac2_by_tactic: [
| "by" ltac2_expr5      (* ltac2 plugin *)
]

ltac2_entry: [
]

ltac2_selector: [
| toplevel_selector ":"
]

ltac2_use_default: [
| "."      (* ltac2 plugin *)
| "..."      (* ltac2 plugin *)
]

tac2def_body: [
| [ "_" | ident ] LIST0 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr      (* ltac2 plugin *)
]

tac2typ_def: [
| OPT tac2typ_prm qualid OPT ( [ ":=" | "::=" ] tac2typ_knd )      (* ltac2 plugin *)
]

tac2typ_prm: [
| ltac2_typevar      (* ltac2 plugin *)
| "(" LIST1 ltac2_typevar SEP "," ")"      (* ltac2 plugin *)
]

tac2typ_knd: [
| ltac2_type      (* ltac2 plugin *)
| "[" OPT ( OPT "|" LIST1 tac2alg_constructor SEP "|" ) "]"      (* ltac2 plugin *)
| "[" ".." "]"      (* ltac2 plugin *)
| "{" OPT ( LIST1 tac2rec_field SEP ";" OPT ";" ) "}"      (* ltac2 plugin *)
]

tac2alg_constructor: [
| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident      (* ltac2 plugin *)
| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident "(" LIST0 ltac2_type SEP "," ")"      (* ltac2 plugin *)
]

tac2rec_field: [
| OPT "mutable" ident ":" ltac2_type      (* ltac2 plugin *)
]

ltac2_syntax_class: [
| string      (* ltac2 plugin *)
| integer      (* ltac2 plugin *)
| name      (* Ltac2 plugin *)
| name "(" LIST1 ltac2_syntax_class SEP "," ")"      (* Ltac2 plugin *)
]

ltac2_expr: [
| ltac2_expr5 ";" ltac2_expr      (* ltac2 plugin *)
| ltac2_expr5      (* ltac2 plugin *)
]

ltac2_expr5: [
| "fun" LIST1 tac2pat0 OPT ( ":" ltac2_type ) "=>" ltac2_expr      (* ltac2 plugin *)
| "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr      (* Ltac2 plugin *)
| ltac2_expr3      (* ltac2 plugin *)
]

ltac2_let_clause: [
| LIST1 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr      (* ltac2 plugin *)
]

ltac2_expr3: [
| LIST1 ltac2_expr2 SEP ","      (* Ltac2 plugin *)
]

ltac2_expr2: [
| ltac2_expr1 "::" ltac2_expr2      (* ltac2 plugin *)
| ltac2_expr1      (* ltac2 plugin *)
]

ltac2_expr1: [
| ltac2_expr0 LIST1 ltac2_expr0      (* ltac2 plugin *)
| ltac2_expr0 ".(" qualid ")"      (* ltac2 plugin *)
| ltac2_expr0 ".(" qualid ")" ":=" ltac2_expr5      (* ltac2 plugin *)
| ltac2_expr0      (* ltac2 plugin *)
]

tac2rec_fieldexpr: [
| qualid OPT [ ":=" ltac2_expr1 ]      (* ltac2 plugin *)
]

ltac2_expr0: [
| "(" ltac2_expr ")"      (* ltac2 plugin *)
| "(" ltac2_expr ":" ltac2_type ")"      (* ltac2 plugin *)
| "()"      (* ltac2 plugin *)
| "[" "|" LIST0 ltac2_expr5 SEP ";" "|" "]"      (* ltac2 plugin *)
| "[" LIST0 ltac2_expr5 SEP ";" "]"      (* ltac2 plugin *)
| "{" ltac2_expr0 "with" OPT ( LIST1 tac2rec_fieldexpr SEP ";" OPT ";" ) "}"      (* ltac2 plugin *)
| "{" OPT ( LIST1 tac2rec_fieldexpr SEP ";" OPT ";" ) "}"      (* ltac2 plugin *)
| ltac2_atom      (* ltac2 plugin *)
]

tac2rec_fieldpats: [
| tac2rec_fieldpat ";" OPT tac2rec_fieldpats      (* ltac2 plugin *)
| tac2rec_fieldpat ";"      (* ltac2 plugin *)
| tac2rec_fieldpat      (* ltac2 plugin *)
]

tac2rec_fieldpat: [
| qualid OPT [ ":=" tac2pat1 ]      (* ltac2 plugin *)
]

ltac2_atom: [
| integer      (* ltac2 plugin *)
| string      (* ltac2 plugin *)
| qualid      (* ltac2 plugin *)
| "@" ident      (* ltac2 plugin *)
| "&" ident      (* ltac2 plugin *)
| "'" term      (* ltac2 plugin *)
| ltac2_quotations
]

ltac2_quotations: [
| "ident" ":" "(" ident ")"
| "constr" ":" "(" term ")"
| "open_constr" ":" "(" term ")"
| "preterm" ":" "(" term ")"
| "pat" ":" "(" cpattern ")"
| "reference" ":" "(" [ "&" ident | qualid ] ")"
| "ltac1" ":" "(" ltac1_expr_in_env ")"
| "ltac1val" ":" "(" ltac1_expr_in_env ")"
]

ltac1_expr_in_env: [
| ltac_expr      (* ltac2_ltac1 plugin *)
| LIST0 ident "|-" ltac_expr      (* ltac2_ltac1 plugin *)
]

generic_tactic: [
| ltac_expr
]

ltac2_branches: [
| OPT "|" LIST1 ( OPT atomic_tac2pat "=>" ltac2_expr ) SEP "|"
]

tac2pat1: [
| qualid LIST1 tac2pat0      (* ltac2 plugin *)
| qualid      (* ltac2 plugin *)
| tac2pat0 "::" tac2pat0      (* ltac2 plugin *)
| tac2pat0 "|" LIST1 tac2pat1 SEP "|"      (* ltac2 plugin *)
| tac2pat0 "as" ident      (* ltac2 plugin *)
| tac2pat0      (* ltac2 plugin *)
]

tac2pat0: [
| "_"      (* ltac2 plugin *)
| "()"      (* ltac2 plugin *)
| integer      (* ltac2 plugin *)
| string      (* ltac2 plugin *)
| qualid      (* ltac2 plugin *)
| "(" OPT atomic_tac2pat ")"      (* ltac2 plugin *)
| "{" OPT tac2rec_fieldpats "}"      (* ltac2 plugin *)
| "[" LIST0 tac2pat1 SEP ";" "]"      (* ltac2 plugin *)
]

atomic_tac2pat: [
| tac2pat1 ":" ltac2_type      (* ltac2 plugin *)
| tac2pat1 "," LIST0 tac2pat1 SEP ","      (* ltac2 plugin *)
| tac2pat1      (* ltac2 plugin *)
]

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

rewrite_occs: [
| LIST1 integer
| ident
]

rewstrategy: [
| "fix" ident ":=" rewstrategy1
| LIST1 rewstrategy1 SEP ";"
]

rewstrategy1: [
| "<-" one_term
| "progress" rewstrategy1
| "try" rewstrategy1
| "choice" LIST1 rewstrategy0
| "repeat" rewstrategy1
| "any" rewstrategy1
| "subterm" rewstrategy1
| "subterms" rewstrategy1
| "innermost" rewstrategy1
| "outermost" rewstrategy1
| "bottomup" rewstrategy1
| "topdown" rewstrategy1
| "hints" ident
| "terms" LIST0 one_term
| "eval" red_expr
| "fold" one_term
| rewstrategy0
| "old_hints" ident
]

rewstrategy0: [
| one_term
| "fail"
| "id"
| "refl"
| "(" rewstrategy ")"
]

l3_tactic: [
]

l2_tactic: [
]

l1_tactic: [
]

value_tactic: [
]

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

ltac_expr: [
| ltac_expr4
]

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

ltac_expr3: [
| l3_tactic
| ltac_expr2
]

ltac_expr2: [
| ltac_expr1 "+" ltac_expr2
| ltac_expr1 "||" ltac_expr2
| 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: [
| integer
| 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: [
| goal_selector
| "all"
| "!"
| "par"
]

goal_selector: [
| LIST1 range_selector SEP ","
]

range_selector: [
| natural
| "[" ident "]"
| natural "-" natural
]

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
]