Quelle  fullGrammar   Sprache: C

(* Coq grammar generated from .mlg files.  Do not edit by hand.  Not compiled into Coq *)
DOC_GRAMMAR

Constr.ident: [
| Prim.ident
]

Prim.name: [
| "_"
]

global: [
| Prim.reference
]

constr_pattern: [
| constr
]

cpattern: [
| lconstr
]

sort: [
| "Set"
| "Prop"
| "SProp"
| "Type"
| "Type" "@{" "_" "}"
| "Type" "@{" test_old_sort_qvar reference "|" universe "}"
| "Type" "@{" test_sort_qvar reference ";" universe "}"
| "Type" "@{" universe "}"
]

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

universe_increment: [
| "+" natural
|
]

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

universe_expr: [
| universe_name universe_increment
]

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

lconstr: [
| term200
]

constr: [
| term8
| "@" global univ_annot
]

term200: [
| term100
]

term100: [
| term99 "<:" term200
| term99 "<<:" term200
| term99 ":>" term200
| term99 ":" term200
| term99
]

term99: [
| term90
]

term90: [
| term10
]

term10: [
| term9 LIST1 arg
| "@" global univ_annot LIST0 term9
| "@" pattern_ident LIST1 identref
| binder_constr
| term9
]

term9: [
| ".." term0 ".."
| term8
]

term8: [
| term1
]

term1: [
| term0 ".(" global univ_annot LIST0 arg ")"
| term0 ".(" "@" global univ_annot LIST0 ( term9 ) ")"
| term0 "%" IDENT
| term0 "%_" IDENT
| term0
]

term0: [
| atomic_constr
| term_match
| reference univ_annot
| NUMBER
| string
| "(" term200 ")"
| "{|" record_declaration bar_cbrace
| "`{" term200 "}"
| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot
| "`(" term200 ")"
| "ltac" ":" "(" Pltac.ltac_expr ")"
]

array_elems: [
| LIST0 lconstr SEP ";"
]

record_declaration: [
| fields_def
]

fields_def: [
| field_def ";" fields_def
| field_def
|
]

field_def: [
| global binders ":=" lconstr
]

binder_constr: [
| "forall" open_binders "," term200
| "fun" open_binders "=>" term200
| "let" name binders let_type_cstr ":=" term200 "in" term200
| "let" "fix" fix_decl "in" term200
| "let" "cofix" cofix_body "in" term200
| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
| "let" "'" pattern200 ":=" term200 "in" term200
| "let" "'" pattern200 ":=" term200 case_type "in" term200
| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
| "if" term200 as_return_type "then" term200 "else" term200
| "fix" fix_decls
| "cofix" cofix_decls
]

arg: [
| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
| test_lpar_nat_coloneq "(" natural ":=" lconstr ")"
| term9
]

atomic_constr: [
| sort
| "_"
| "?" "[" identref "]"
| "?" "[" pattern_ident "]"
| pattern_ident evar_instance
]

inst: [
| identref ":=" lconstr
]

evar_instance: [
| "@{" LIST1 inst SEP ";" "}"
|
]

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

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

fix_decls: [
| fix_decl
| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
]

cofix_decls: [
| cofix_body
| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref
]

fix_decl: [
| identref binders_fixannot type_cstr ":=" term200
]

cofix_body: [
| identref binders type_cstr ":=" term200
]

term_match: [
| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
]

case_item: [
| term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
]

case_type: [
| "return" term100
]

as_return_type: [
| OPT [ OPT [ "as" name ] case_type ]
]

branches: [
| OPT "|" LIST0 eqn SEP "|"
]

mult_pattern: [
| LIST1 pattern200 SEP ","
]

eqn: [
| LIST1 mult_pattern SEP "|" "=>" lconstr
]

record_pattern: [
| global ":=" pattern200
]

record_patterns: [
| record_pattern ";" record_patterns
| record_pattern
|
]

pattern200: [
| pattern100
]

pattern100: [
| pattern99 ":" term200
| pattern99
]

pattern99: [
| pattern90
]

pattern90: [
| pattern10
]

pattern10: [
| pattern1 "as" name
| pattern1 LIST1 pattern1
| "@" Prim.reference LIST0 pattern1
| pattern1
]

pattern1: [
| pattern0 "%" IDENT
| pattern0 "%_" IDENT
| pattern0
]

pattern0: [
| Prim.reference
| "{|" record_patterns bar_cbrace
| "_"
| "(" pattern200 ")"
| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
| NUMBER
| string
]

fixannot: [
| "{" "struct" identref "}"
| "{" "wf" constr identref "}"
| "{" "measure" constr OPT identref OPT constr "}"
]

binders_fixannot: [
| ensure_fixannot fixannot
| binder binders_fixannot
|
]

open_binders: [
| name LIST0 name ":" lconstr
| name LIST0 name binders
| name ".." name
| closed_binder binders
]

binders: [
| LIST0 binder
| Procq.Constr.binders
]

binder: [
| name
| closed_binder
]

closed_binder: [
| "(" name LIST1 name ":" lconstr ")"
| "(" name ":" lconstr ")"
| "(" name ":=" lconstr ")"
| "(" name ":" lconstr ":=" lconstr ")"
| "(" name ":" lconstr "|" lconstr ")"
| "{" name "}"
| "{" name LIST1 name ":" lconstr "}"
| "{" name ":" lconstr "}"
| "{" name LIST1 name "}"
| "[" name "]"
| "[" name LIST1 name ":" lconstr "]"
| "[" name ":" lconstr "]"
| "[" name LIST1 name "]"
| "`(" LIST1 typeclass_constraint SEP "," ")"
| "`{" LIST1 typeclass_constraint SEP "," "}"
| "`[" LIST1 typeclass_constraint SEP "," "]"
| "'" pattern0
]

one_open_binder: [
| name
| name ":" lconstr
| one_closed_binder
]

one_closed_binder: [
| "(" name ":" lconstr ")"
| "{" name "}"
| "{" name ":" lconstr "}"
| "[" name "]"
| "[" name ":" lconstr "]"
| "'" pattern0
]

typeclass_constraint: [
| "!" term200
| "{" name "}" ":" [ "!" | ] term200
| test_name_colon name ":" [ "!" | ] term200
| term200
]

type_cstr: [
| ":" lconstr
|
]

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

preident: [
| IDENT
]

ident: [
| IDENT
]

pattern_ident: [
| LEFTQMARK ident
]

identref: [
| ident
]

hyp: [
| identref
]

field: [
| FIELD
]

fields: [
| field fields
| field
]

fullyqualid: [
| ident fields
| ident
]

name: [
| "_"
| ident
]

reference: [
| ident fields
| ident
]

qualid: [
| reference
]

by_notation: [
| ne_string OPT [ "%" IDENT ]
]

smart_global: [
| reference
| by_notation
]

ne_string: [
| STRING
]

ne_lstring: [
| ne_string
]

dirpath: [
| ident LIST0 field
]

string: [
| STRING
]

lstring: [
| string
]

integer: [
| bigint
]

natural: [
| bignat
]

bigint: [
| bignat
| test_minus_nat "-" bignat
]

bignat: [
| NUMBER
]

bar_cbrace: [
| test_pipe_closedcurly "|" "}"
]

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

vernac_toplevel: [
| "Drop" "."
| "Quit" "."
| "BackTo" natural "."
| test_show_goal "Show" "Goal" natural "at" natural "."
| "Show" "Proof" "Diffs" OPT "removed" "."
| Pvernac.Vernac_.main_entry
]

opt_hintbases: [
|
| ":" LIST1 IDENT
]

command: [
| "Goal" lconstr
| "Proof"
| "Proof" "using" G_vernac.section_subset_expr
| "Proof" "with" generic_tactic OPT [ "using" G_vernac.section_subset_expr ]
| "Proof" "using" G_vernac.section_subset_expr "with" generic_tactic
| "Proof" "Mode" string
| "Proof" lconstr
| "Abort"
| "Abort" "All"
| "Admitted"
| "Qed"
| "Save" identref
| "Defined"
| "Defined" identref
| "Restart"
| "Undo"
| "Undo" natural
| "Undo" "To" natural
| "Focus"
| "Focus" natural
| "Unfocus"
| "Unfocused"
| "Show"
| "Show" natural
| "Show" ident
| "Show" "Existentials"
| "Show" "Universes"
| "Show" "Conjectures"
| "Show" "Proof"
| "Show" "Intro"
| "Show" "Intros"
| "Show" "Match" reference
| "Guarded"
| "Validate" "Proof"
| "Create" "HintDb" IDENT; [ "discriminated" | ]
| "Remove" "Hints" LIST1 global opt_hintbases
| "Hint" hint opt_hintbases
| "Comments" LIST0 comment
| "Attributes" attribute_list
| "Declare" "Instance" ident_decl binders ":" term200 hint_info
| "Declare" "Scope" IDENT
| "Pwd"
| "Cd"
| "Cd" ne_string
| "Load" [ "Verbose" | ] [ ne_string | IDENT ]
| "Declare" "ML" "Module" LIST1 ne_string
| "Locate" locatable
| "Type" lconstr
| "Print" printable
| "Print" smart_global OPT univ_name_list
| "Print" "Module" "Type" global
| "Print" "Module" global
| "Print" "Namespace" dirpath
| "Inspect" natural
| "Set" setting_name option_setting
| "Unset" setting_name
| "Print" "Table" setting_name
| "Add" IDENT IDENT LIST1 table_value
| "Add" IDENT LIST1 table_value
| "Test" setting_name "for" LIST1 table_value
| "Test" setting_name
| "Remove" IDENT IDENT LIST1 table_value
| "Remove" IDENT LIST1 table_value
| "Reset" "Initial"
| "Reset" identref
| "Back"
| "Back" natural
| "Debug" "On"
| "Debug" "Off"
| "Declare" "Reduction" IDENT; ":=" red_expr
| "Declare" "Custom" "Entry" IDENT
| "Obligation" natural "of" identref withtac
| "Obligation" natural withtac
| "Next" "Obligation" "of" identref withtac
| "Next" "Obligation" withtac
| "Final" "Obligation" "of" identref withtac
| "Final" "Obligation" withtac
| "Solve" "Obligations" "of" identref withtac
| "Solve" "Obligations" withtac
| "Solve" "All" "Obligations" withtac
| "Admit" "Obligations" "of" identref
| "Admit" "Obligations"
| "Obligation" "Tactic" ":=" generic_tactic
| "Show" "Obligation" "Tactic"
| "Obligations" "of" identref
| "Obligations"
| "Preterm" "of" identref
| "Preterm"
| "Derive" open_binders "SuchThat" constr "As" identref      (* derive plugin *)
| "Derive" open_binders "in" constr "as" identref      (* derive plugin *)
| "Extraction" global      (* extraction plugin *)
| "Recursive" "Extraction" LIST1 global      (* extraction plugin *)
| "Extraction" string LIST1 global      (* extraction plugin *)
| "Extraction" "TestCompile" LIST1 global      (* extraction plugin *)
| "Separate" "Extraction" LIST1 global      (* extraction plugin *)
| "Extraction" "Library" identref      (* extraction plugin *)
| "Recursive" "Extraction" "Library" identref      (* extraction plugin *)
| "Extraction" "Language" language      (* extraction plugin *)
| "Extraction" "Inline" LIST1 global      (* extraction plugin *)
| "Extraction" "NoInline" LIST1 global      (* extraction plugin *)
| "Print" "Extraction" "Inline"      (* extraction plugin *)
| "Reset" "Extraction" "Inline"      (* extraction plugin *)
| "Extraction" "Implicit" global "[" LIST0 int_or_id "]"      (* extraction plugin *)
| "Extraction" "Blacklist" LIST1 preident      (* extraction plugin *)
| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
| "Extract" "Callback" OPT string global      (* extraction plugin *)
| "Print" "Extraction" "Callback"      (* extraction plugin *)
| "Reset" "Extraction" "Callback"      (* extraction plugin *)
| "Print" "Extraction" "Foreign"      (* extraction plugin *)
| "Extract" "Constant" global LIST0 string "=>" mlname      (* extraction plugin *)
| "Extract" "Foreign" "Constant" global "=>" string      (* extraction plugin *)
| "Extract" "Inlined" "Constant" global "=>" mlname      (* extraction plugin *)
| "Extract" "Inductive" global "=>" mlname "[" LIST0 mlname "]" OPT string      (* extraction plugin *)
| "Show" "Extraction"      (* extraction plugin *)
| "Set" "Firstorder" "Solver" generic_tactic
| "Print" "Firstorder" "Solver"
| "Function" LIST1 function_fix_definition SEP "with"      (* funind plugin *)
| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"      (* funind plugin *)
| "Functional" "Case" fun_scheme_arg      (* funind plugin *)
| "Generate" "graph" "for" reference      (* funind plugin *)
| "Hint" "Rewrite" orient LIST1 constr ":" LIST1 preident
| "Hint" "Rewrite" orient LIST1 constr "using" generic_tactic ":" LIST1 preident
| "Hint" "Rewrite" orient LIST1 constr
| "Hint" "Rewrite" orient LIST1 constr "using" generic_tactic
| "Derive" "Inversion_clear" identref "with" constr "Sort" sort_quality_or_set
| "Derive" "Inversion_clear" identref "with" constr
| "Derive" "Inversion" identref "with" constr "Sort" sort_quality_or_set
| "Derive" "Inversion" identref "with" constr
| "Derive" "Dependent" "Inversion" identref "with" constr "Sort" sort_quality_or_set
| "Derive" "Dependent" "Inversion_clear" identref "with" constr "Sort" sort_quality_or_set
| "Declare" "Left" "Step" constr
| "Declare" "Right" "Step" constr
| "Unshelve"
| "Declare" "Equivalent" "Keys" constr constr
| "Print" "Equivalent" "Keys"
| "Optimize" "Proof"
| "Optimize" "Heap"
| "infoH" tactic
| "Hint" "Cut" "[" hints_path "]" opthints
| "Typeclasses" "Transparent" LIST1 reference
| "Typeclasses" "Opaque" LIST1 reference
| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural
| "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
| "Print" "Ltac" reference
| "Locate" "Ltac" reference
| "Ltac" LIST1 ltac_tacdef_body SEP "with"
| "Print" "Ltac" "Signatures"
| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" identref
| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" identref
| "Add" "Relation" constr constr "as" identref
| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" identref
| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" identref
| "Add" "Setoid" constr constr constr "as" identref
| "Add" "Parametric" "Setoid" binders ":" constr constr constr "as" identref
| "Add" "Morphism" constr ":" identref
| "Declare" "Morphism" constr ":" identref
| "Add" "Morphism" constr "with" "signature" lconstr "as" identref
| "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" identref
| "Print" "Rewrite" "HintDb" preident
| "Reset" "Ltac" "Profile"
| "Show" "Ltac" "Profile"
| "Show" "Ltac" "Profile" "CutOff" integer
| "Show" "Ltac" "Profile" string
| "Show" "Lia" "Profile"      (* micromega plugin *)
| "Add" "Zify" "InjTyp" reference      (* micromega plugin *)
| "Add" "Zify" "BinOp" reference      (* micromega plugin *)
| "Add" "Zify" "UnOp" reference      (* micromega plugin *)
| "Add" "Zify" "CstOp" reference      (* micromega plugin *)
| "Add" "Zify" "BinRel" reference      (* micromega plugin *)
| "Add" "Zify" "PropOp" reference      (* micromega plugin *)
| "Add" "Zify" "PropBinOp" reference      (* micromega plugin *)
| "Add" "Zify" "PropUOp" reference      (* micromega plugin *)
| "Add" "Zify" "BinOpSpec" reference      (* micromega plugin *)
| "Add" "Zify" "UnOpSpec" reference      (* micromega plugin *)
| "Add" "Zify" "Saturate" reference      (* 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" "UnOpSpec"      (* micromega plugin *)
| "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
| "Add" "Ring" identref ":" constr OPT ring_mods      (* ring plugin *)
| "Print" "Rings"      (* ring plugin *)
| "Add" "Field" identref ":" constr OPT field_mods      (* ring plugin *)
| "Print" "Fields"      (* ring plugin *)
| "Number" "Notation" reference reference reference OPT number_options ":" preident
| "String" "Notation" reference reference reference OPT string_option ":" preident
| "Ltac2" ltac2_entry      (* ltac2 plugin *)
| "Ltac2" "Notation" ltac2def_syn      (* ltac2 plugin *)
| "Ltac2" "Eval" ltac2_expr6      (* ltac2 plugin *)
| "Print" test_ltac2_ident "Ltac2" reference      (* ltac2 plugin *)
| "Print" "Ltac2" "Type" reference      (* ltac2 plugin *)
| "Locate" "Ltac2" reference      (* ltac2 plugin *)
| "Print" "Ltac2" "Signatures"      (* ltac2 plugin *)
| "Ltac2" "Check" ltac2_expr6      (* ltac2 plugin *)
| "Ltac2" "Globalize" ltac2_expr6      (* ltac2 plugin *)
]

reference_or_constr: [
| global
| constr
]

hint: [
| "Resolve" LIST1 reference_or_constr hint_info
| "Resolve" "->" LIST1 global OPT natural
| "Resolve" "<-" LIST1 global OPT natural
| "Immediate" LIST1 reference_or_constr
| "Variables" "Transparent"
| "Variables" "Opaque"
| "Constants" "Transparent"
| "Constants" "Opaque"
| "Projections" "Transparent"
| "Projections" "Opaque"
| "Transparent" LIST1 global
| "Opaque" LIST1 global
| "Mode" global mode
| "Unfold" LIST1 global
| "Constructors" LIST1 global
| "Extern" natural OPT Constr.constr_pattern "=>" generic_tactic
]

mode: [
| LIST1 [ "+" | "!" | "-" ]
]

int_or_var: [
| integer
| identref
]

nat_or_var: [
| natural
| identref
]

occs_nums: [
| LIST1 nat_or_var
| "-" LIST1 nat_or_var
]

occs: [
| "at" occs_nums
|
]

pattern_occ: [
| constr occs
]

ref_or_pattern_occ: [
| smart_global occs
| constr occs
]

unfold_occ: [
| smart_global occs
]

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

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

strategy_flag: [
| LIST1 red_flag
| OPT "head" delta_flag
]

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

vernac_control: [
| "Time" vernac_control
| "Instructions" vernac_control
| "Profile" OPT STRING vernac_control
| "Redirect" ne_string vernac_control
| "Timeout" natural vernac_control
| "Fail" vernac_control
| "Succeed" vernac_control
| decorated_vernac
]

decorated_vernac: [
| quoted_attributes LIST0 legacy_attr vernac_aux
]

quoted_attributes: [
| LIST0 [ "#[" attribute_list "]" ]
]

attribute_list: [
| LIST1 attribute SEP ","
]

attribute: [
| ident attr_value
| "using" attr_value
]

attr_value: [
| "=" string
| "=" qualid
| "(" attribute_list ")"
|
]

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

vernac_aux: [
| gallina "."
| gallina_ext "."
| command "."
| syntax "."
| command_entry
]

noedit_mode: [
| query_command
]

subprf: [
| BULLET
| "}"
]

subprf_with_selector: [
| "{"
| query_command
]

gallina: [
| thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
| assumption_token inline assum_list
| assumptions_token inline assum_list
| def_token ident_decl def_body
| "Symbol" assum_list
| "Symbols" assum_list
| "Let" ident_decl def_body
| finite_token inductive_or_record_definition
| inductive_token LIST1 inductive_or_record_definition SEP "with"
| "Fixpoint" LIST1 fix_definition SEP "with"
| "Let" "Fixpoint" LIST1 fix_definition SEP "with"
| "CoFixpoint" LIST1 cofix_definition SEP "with"
| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with"
| "Scheme" LIST1 scheme SEP "with"
| "Scheme" "Equality" "for" smart_global
| "Scheme" "Boolean" "Equality" "for" smart_global
| "Combined" "Scheme" identref "from" LIST1 identref SEP ","
| "Register" global "as" qualid
| "Register" "Scheme" global "as" qualid "for" global
| "Register" "Inline" global
| "Primitive" ident_decl OPT [ ":" lconstr ] ":=" register_token
| "Universe" LIST1 identref
| "Universes" LIST1 identref
| "Sort" LIST1 identref
| "Sorts" LIST1 identref
| "Constraint" LIST1 univ_constraint SEP ","
| "Rewrite" "Rule" identref ":=" OPT "|" LIST1 rewrite_rule SEP "|"
| "Rewrite" "Rules" identref ":=" OPT "|" LIST1 rewrite_rule SEP "|"
]

register_token: [
| test_hash_ident "#" IDENT
]

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

def_token: [
| "Definition"
| "Example"
| "SubClass"
]

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

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

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

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

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

univ_decl: [
| "@{" test_doublepipe_univ_decl LIST0 identref "|" LIST0 identref [ "+" | ] univ_decl_constraints
| "@{" LIST0 identref ";" LIST0 identref [ "+" | ] univ_decl_constraints
| "@{" LIST0 identref [ "+" | ] univ_decl_constraints
]

variance: [
| "+"
| "="
| "*"
]

variance_identref: [
| identref
| test_variance_ident variance identref
]

cumul_univ_decl: [
| "@{" test_doublepipe_cumul_univ_decl LIST0 identref "|" LIST0 variance_identref [ "+" | ] univ_decl_constraints
| "@{" test_semicolon_cumul_univ_decl LIST0 identref ";" LIST0 variance_identref [ "+" | ] univ_decl_constraints
| "@{" LIST0 variance_identref [ "+" | ] univ_decl_constraints
]

ident_decl: [
| identref OPT univ_decl
]

cumul_ident_decl: [
| identref OPT cumul_univ_decl
]

inductive_token: [
| "Inductive"
| "CoInductive"
]

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

def_body: [
| binders ":=" reduce lconstr
| binders ":" lconstr ":=" reduce lconstr
| binders ":" lconstr
]

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

notation_declaration: [
| lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
]

decl_sep: [
| "and"
]

decl_notations: [
| "where" LIST1 notation_declaration SEP decl_sep
|
]

opt_constructors_or_fields: [
| ":=" constructors_or_record
| ":="
|
]

inductive_or_record_definition: [
| opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
]

constructors_or_record: [
| "|" LIST1 constructor SEP "|"
| quoted_attributes identref constructor_type "|" LIST1 constructor SEP "|"
| quoted_attributes identref constructor_type
| quoted_attributes identref "{" record_fields "}" default_inhabitant_ident
| "{" record_fields "}" default_inhabitant_ident
]

default_inhabitant_ident: [
| "as" identref
|
]

opt_coercion: [
| ">"
|
]

fix_definition: [
| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
]

cofix_definition: [
| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
]

rw_pattern: [
| lconstr
]

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

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

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

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

record_field: [
| quoted_attributes record_binder OPT [ "|" natural ] decl_notations
]

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

field_body: [
| binders of_type_inst lconstr
| binders of_type_inst lconstr ":=" lconstr
| binders ":=" lconstr
]

record_binder: [
| name
| name field_body
]

assum_list: [
| LIST1 assum_coe
| assumpt
]

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

assumpt: [
| LIST1 ident_decl of_type lconstr
]

constructor_type: [
| binders [ of_type_inst lconstr | ]
]

constructor: [
| quoted_attributes identref constructor_type
]

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

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

gallina_ext: [
| "Module" export_token identref LIST0 module_binder of_module_type is_module_expr
| "Module" "Type" identref LIST0 module_binder check_module_types is_module_type
| "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl
| "Section" identref
| "End" identref
| "Collection" identref ":=" section_subset_expr
| "From" global "Extra" "Dependency" ne_string OPT [ "as" IDENT ]
| "Require" export_token LIST1 filtered_import
| "From" global "Require" export_token LIST1 filtered_import
| "Import" OPT import_categories LIST1 filtered_import
| "Export" OPT import_categories LIST1 filtered_import
| "Include" module_type_inl LIST0 ext_module_type
| "Include" "Type" module_type_inl LIST0 ext_module_type
| "Transparent" OPT "!" LIST1 smart_global
| "Opaque" OPT "!" LIST1 smart_global
| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
| "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ]
| "Canonical" OPT "Structure" by_notation
| "Coercion" global OPT [ OPT univ_decl def_body ]
| "Identity" "Coercion" identref ":" coercion_class ">->" coercion_class
| "Coercion" global ":" coercion_class ">->" coercion_class
| "Coercion" by_notation ":" coercion_class ">->" coercion_class
| "Context" LIST1 binder
| "Instance" instance_name ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
| "Existing" "Instance" global hint_info
| "Existing" "Instances" LIST1 global OPT [ "|" natural ]
| "Existing" "Class" global
| "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ]
| "Implicit" "Type" reserv_list
| "Implicit" "Types" reserv_list
| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
| "Export" "Set" setting_name option_setting
| "Export" "Unset" setting_name
]

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

filtered_import: [
| global
| global "(" LIST1 one_import_filter_name SEP "," ")"
]

one_import_filter_name: [
| global OPT [ "(" ".." ")" ]
]

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

ext_module_type: [
| "<+" module_type_inl
]

ext_module_expr: [
| "<+" module_expr_inl
]

check_module_type: [
| "<:" module_type_inl
]

check_module_types: [
| LIST0 check_module_type
]

of_module_type: [
| ":" module_type_inl
| check_module_types
]

is_module_type: [
| ":=" module_type_inl LIST0 ext_module_type
|
]

is_module_expr: [
| ":=" module_expr_inl LIST0 ext_module_expr
|
]

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

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

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

module_binder: [
| "(" export_token LIST1 identref ":" module_type_inl ")"
]

module_expr: [
| module_expr_atom
| module_expr module_expr_atom
]

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

with_declaration: [
| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr
| "Module" fullyqualid ":=" qualid
]

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

section_subset_expr: [
| test_only_starredidentrefs LIST0 starredidentref
| ssexpr35
]

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

ssexpr35: [
| "-" ssexpr50
| ssexpr50
]

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

ssexpr0: [
| starredidentref
| "()"
| "(" test_only_starredidentrefs LIST0 starredidentref ")"
| "(" test_only_starredidentrefs LIST0 starredidentref ")" "*"
| "(" ssexpr35 ")"
| "(" ssexpr35 ")" "*"
]

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_delimiter: [
| "%" IDENT
| "%_" IDENT
]

argument_spec: [
| OPT "!" name LIST0 scope_delimiter
]

arg_specs: [
| argument_spec
| "/"
| "&"
| "(" LIST1 argument_spec ")" LIST0 scope_delimiter
| "[" LIST1 argument_spec "]" LIST0 scope_delimiter
| "{" LIST1 argument_spec "}" LIST0 scope_delimiter
]

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

instance_name: [
| ident_decl binders
|
]

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

reserv_list: [
| LIST1 reserv_tuple
| simple_reserv
]

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

simple_reserv: [
| LIST1 identref ":" lconstr
]

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

goal_selector: [
| LIST1 range_selector SEP ","
]

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

query_command: [
| "Eval" red_expr "in" lconstr "."
| "Compute" lconstr "."
| "Check" lconstr "."
| "About" smart_global OPT univ_name_list "."
| "SearchPattern" constr_pattern in_or_out_modules "."
| "SearchRewrite" constr_pattern in_or_out_modules "."
| "Search" search_query search_queries "."
]

printable: [
| "Term" smart_global OPT univ_name_list
| "All"
| "Section" global
| "Grammar" LIST0 IDENT
| "Custom" "Grammar" IDENT
| "Keywords"
| "LoadPath" OPT dirpath
| "Libraries"
| "Notation" string
| "Notation" string "in" "custom" IDENT
| "ML" "Path"
| "ML" "Modules"
| "Debug" "GC"
| "Graph"
| "Classes"
| "Typeclasses"
| "Instances" smart_global
| "Coercions"
| "Coercion" "Paths" coercion_class coercion_class
| "Canonical" "Projections" LIST0 smart_global
| "Typing" "Flags"
| "Tables"
| "Options"
| "Hint"
| "Hint" smart_global
| "Hint" "*"
| "HintDb" IDENT
| "Scopes"
| "Scope" IDENT
| "Visibility" OPT IDENT
| "Implicit" smart_global
| [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT [ [ "With" | "Without" ] "Constraint" "Sources" ] OPT ne_string
| "Sorts"
| "Assumptions" smart_global
| "Opaque" "Dependencies" smart_global
| "Transparent" "Dependencies" smart_global
| "All" "Dependencies" smart_global
| "Strategy" smart_global
| "Strategies"
| "Registered"
| "Registered" "Schemes"
]

debug_univ_name: [
| reference
| STRING
]

printunivs_subgraph: [
| "Subgraph" "(" LIST0 debug_univ_name ")"
]

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

locatable: [
| smart_global
| "Term" smart_global
| "File" ne_string
| "Library" global
| "Module" global
]

option_setting: [
|
| integer
| STRING
]

table_value: [
| global
| STRING
]

setting_name: [
| LIST1 IDENT
]

ne_in_or_out_modules: [
| "inside" LIST1 global
| "in" LIST1 global
| "outside" LIST1 global
]

in_or_out_modules: [
| ne_in_or_out_modules
|
]

comment: [
| constr
| STRING
| natural
]

positive_search_mark: [
| "-"
|
]

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

search_item: [
| test_id_colon search_where ":" ne_string OPT scope_delimiter
| "is" ":" logical_kind
| ne_string OPT scope_delimiter
| test_id_colon search_where ":" constr_pattern
| constr_pattern
]

logical_kind: [
| thm_token
| assumption_token
| "Context"
| extended_def_token
| "Primitive"
| "Symbol"
]

extended_def_token: [
| def_token
| "Coercion"
| "Fixpoint"
| "CoFixpoint"
| "Instance"
| "Scheme"
| "Canonical"
| "Field"
| "Method"
]

search_where: [
| "head"
| "hyp"
| "concl"
| "headhyp"
| "headconcl"
]

search_queries: [
| ne_in_or_out_modules
| search_query search_queries
|
]

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

syntax: [
| "Open" "Scope" IDENT
| "Close" "Scope" IDENT
| "Delimit" "Scope" IDENT; "with" IDENT
| "Undelimit" "Scope" IDENT
| "Bind" "Scope" IDENT; "with" LIST1 coercion_class
| "Infix" notation_declaration
| "Notation" identref LIST0 ident ":=" constr syntax_modifiers
| "Notation" notation_declaration
| "Reserved" "Infix" ne_lstring syntax_modifiers
| "Reserved" "Notation" ne_lstring syntax_modifiers
| enable_enable_disable "Notation" enable_notation_rule enable_notation_interpretation enable_notation_flags opt_scope
]

enable_enable_disable: [
| "Enable"
| "Disable"
]

enable_notation_rule: [
| ne_string
| global LIST0 ident
|
]

enable_notation_interpretation: [
| ":=" constr
|
]

enable_notation_flags: [
| "(" LIST1 enable_notation_flag SEP "," ")"
|
]

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

opt_scope: [
| ":" IDENT
| ":" "no" "scope"
|
]

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

syntax_modifier: [
| "at" "level" natural
| "in" "custom" IDENT
| "in" "custom" IDENT; "at" "level" natural
| "left" "associativity"
| "right" "associativity"
| "no" "associativity"
| "only" "printing"
| "only" "parsing"
| "format" lstring
| IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
| IDENT; "at" level OPT binder_interp
| IDENT; "in" "scope" IDENT
| IDENT binder_interp
| IDENT explicit_subentry
]

syntax_modifiers: [
| "(" LIST1 syntax_modifier SEP "," ")"
|
]

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

at_level_opt: [
| "at" level
|
]

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

withtac: [
|
| "with" generic_tactic
]

simple_tactic: [
| "btauto"
| "congruence" OPT natural
| "congruence" OPT natural "with" LIST1 constr
| "simple" "congruence" OPT natural
| "simple" "congruence" OPT natural "with" LIST1 constr
| "f_equal"
| "firstorder" OPT tactic firstorder_using
| "firstorder" OPT tactic "with" LIST1 preident
| "firstorder" OPT tactic firstorder_using "with" LIST1 preident
| "functional" "inversion" quantified_hypothesis OPT reference      (* funind plugin *)
| "functional" "induction" lconstr fun_ind_using with_names      (* funind plugin *)
| "soft" "functional" "induction" LIST1 constr fun_ind_using with_names      (* funind plugin *)
| "reflexivity"
| "exact" uconstr
| "assumption"
| "etransitivity"
| "cut" constr
| "exact_no_check" constr
| "vm_cast_no_check" constr
| "native_cast_no_check" constr
| "exfalso"
| "lapply" constr
| "transitivity" constr
| "left"
| "eleft"
| "left" "with" bindings
| "eleft" "with" bindings
| "right"
| "eright"
| "right" "with" bindings
| "eright" "with" bindings
| "constructor"
| "constructor" nat_or_var
| "constructor" nat_or_var "with" bindings
| "econstructor"
| "econstructor" nat_or_var
| "econstructor" nat_or_var "with" bindings
| "specialize" constr_with_bindings
| "specialize" constr_with_bindings "as" simple_intropattern
| "symmetry"
| "symmetry" "in" in_clause
| "split"
| "esplit"
| "split" "with" bindings
| "esplit" "with" bindings
| "exists"
| "exists" LIST1 bindings SEP ","
| "eexists"
| "eexists" LIST1 bindings SEP ","
| "intros" "until" quantified_hypothesis
| "intro"
| "intro" ident
| "intro" ident "at" "top"
| "intro" ident "at" "bottom"
| "intro" ident "after" hyp
| "intro" ident "before" hyp
| "intro" "at" "top"
| "intro" "at" "bottom"
| "intro" "after" hyp
| "intro" "before" hyp
| "move" hyp "at" "top"
| "move" hyp "at" "bottom"
| "move" hyp "after" hyp
| "move" hyp "before" hyp
| "rename" LIST1 rename SEP ","
| "revert" LIST1 hyp
| "simple" "induction" quantified_hypothesis
| "simple" "destruct" quantified_hypothesis
| "admit"
| "fix" ident natural
| "cofix" ident
| "clear" LIST0 hyp
| "clear" "-" LIST1 hyp
| "clearbody" LIST1 hyp
| "generalize" "dependent" constr
| "assert_succeeds" tactic3
| "replace" uconstr "with" constr clause by_arg_tac
| "replace" "->" uconstr clause
| "replace" "->" uconstr "with" constr clause by_arg_tac
| "replace" "<-" uconstr clause
| "replace" "<-" uconstr "with" constr clause by_arg_tac
| "replace" uconstr clause
| "simplify_eq"
| "simplify_eq" destruction_arg
| "esimplify_eq"
| "esimplify_eq" destruction_arg
| "discriminate"
| "discriminate" destruction_arg
| "ediscriminate"
| "ediscriminate" destruction_arg
| "injection"
| "injection" destruction_arg
| "einjection"
| "einjection" destruction_arg
| "injection" "as" LIST0 simple_intropattern
| "injection" destruction_arg "as" LIST0 simple_intropattern
| "einjection" "as" LIST0 simple_intropattern
| "einjection" destruction_arg "as" LIST0 simple_intropattern
| "simple" "injection"
| "simple" "injection" destruction_arg
| "dependent" "rewrite" orient constr
| "dependent" "rewrite" orient constr "in" hyp
| "decompose" "sum" constr
| "decompose" "record" constr
| "absurd" constr
| "contradiction" OPT constr_with_bindings
| "autorewrite" "with" LIST1 preident clause
| "autorewrite" "with" LIST1 preident clause "using" tactic
| "autorewrite" "*" "with" LIST1 preident clause
| "autorewrite" "*" "with" LIST1 preident clause "using" tactic
| "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac
| "rewrite" "*" orient uconstr "at" occurrences "in" hyp by_arg_tac
| "rewrite" "*" orient uconstr "in" hyp by_arg_tac
| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac
| "rewrite" "*" orient uconstr by_arg_tac
| "refine" uconstr
| "simple" "refine" uconstr
| "notypeclasses" "refine" uconstr
| "simple" "notypeclasses" "refine" uconstr
| "solve_constraints"
| "subst" LIST1 hyp
| "subst"
| "simple" "subst"
| "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
| "evar" constr
| "instantiate" "(" ident ":=" lglob ")"
| "instantiate" "(" natural ":=" lglob ")" hloc
| "stepl" constr "by" tactic
| "stepl" constr
| "stepr" constr "by" tactic
| "stepr" constr
| "generalize_eqs" hyp
| "dependent" "generalize_eqs" hyp
| "generalize_eqs_vars" hyp
| "dependent" "generalize_eqs_vars" hyp
| "specialize_eqs" hyp
| "destauto"
| "destauto" "in" hyp
| "transparent_abstract" tactic3
| "transparent_abstract" tactic3 "using" ident
| "constr_eq" constr constr
| "constr_eq_strict" constr constr
| "constr_eq_nounivs" constr constr
| "is_evar" constr
| "has_evar" constr
| "is_var" constr
| "is_fix" constr
| "is_cofix" constr
| "is_ind" constr
| "is_constructor" constr
| "is_proj" constr
| "is_const" constr
| "shelve"
| "shelve_unifiable"
| "unshelve" tactic1
| "give_up"
| "cycle" int_or_var
| "swap" int_or_var int_or_var
| "revgoals"
| "guard" test
| "decompose" "[" LIST1 constr "]" constr
| "optimize_heap"
| "with_strategy" strategy_level_or_var "[" LIST1 smart_global "]" tactic3
| "eassumption"
| "eexact" constr
| "trivial" auto_using hintbases
| "info_trivial" auto_using hintbases
| "debug" "trivial" auto_using hintbases
| "auto" OPT nat_or_var auto_using hintbases
| "info_auto" OPT nat_or_var auto_using hintbases
| "debug" "auto" OPT nat_or_var auto_using hintbases
| "eauto" OPT nat_or_var auto_using hintbases
| "debug" "eauto" OPT nat_or_var auto_using hintbases
| "info_eauto" OPT nat_or_var auto_using hintbases
| "autounfold" hintbases clause_dft_concl
| "autounfold_one" hintbases "in" hyp
| "autounfold_one" hintbases
| "unify" constr constr
| "unify" constr constr "with" preident
| "convert" constr constr
| "typeclasses" "eauto" "dfs" OPT nat_or_var "with" LIST1 preident
| "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident
| "typeclasses" "eauto" "best_effort" OPT nat_or_var "with" LIST1 preident
| "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident
| "typeclasses" "eauto" "bfs" OPT nat_or_var
| "typeclasses" "eauto" "dfs" OPT nat_or_var
| "typeclasses" "eauto" "best_effort" OPT nat_or_var
| "typeclasses" "eauto" OPT nat_or_var
| "head_of_constr" ident constr
| "not_evar" constr
| "is_ground" constr
| "autoapply" constr "with" preident
| "decide" "equality"
| "compare" constr constr
| "rewrite_strat" rewstrategy "in" hyp
| "rewrite_strat" rewstrategy
| "rewrite_db" preident "in" hyp
| "rewrite_db" preident
| "substitute" orient glob_constr_with_bindings
| "setoid_rewrite" orient glob_constr_with_bindings
| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp
| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences
| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp
| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp "at" occurrences
| "setoid_symmetry"
| "setoid_symmetry" "in" hyp
| "setoid_reflexivity"
| "setoid_transitivity" constr
| "setoid_etransitivity"
| "intros" ne_intropatterns
| "intros"
| "eintros" ne_intropatterns
| "eintros"
| "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
| "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
| "elim" constr_with_bindings_arg OPT eliminator
| "eelim" constr_with_bindings_arg OPT eliminator
| "case" induction_clause_list
| "ecase" induction_clause_list
| "fix" ident natural "with" LIST1 fixdecl
| "cofix" ident "with" LIST1 cofixdecl
| "pose" bindings_with_parameters
| "pose" constr as_name
| "epose" bindings_with_parameters
| "epose" constr as_name
| "set" bindings_with_parameters clause_dft_concl
| "set" constr as_name clause_dft_concl
| "eset" bindings_with_parameters clause_dft_concl
| "eset" constr as_name clause_dft_concl
| "remember" constr as_name eqn_ipat clause_dft_all
| "eremember" constr as_name eqn_ipat clause_dft_all
| "assert" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
| "eassert" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
| "assert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
| "eassert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
| "enough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
| "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
| "assert" constr as_ipat by_tactic
| "eassert" constr as_ipat by_tactic
| "pose" "proof" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
| "epose" "proof" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
| "pose" "proof" lconstr as_ipat
| "epose" "proof" lconstr as_ipat
| "enough" constr as_ipat by_tactic
| "eenough" constr as_ipat by_tactic
| "generalize" constr
| "generalize" constr LIST1 constr
| "generalize" constr lookup_at_as_comma occs as_name LIST0 [ "," pattern_occ as_name ]
| "induction" induction_clause_list
| "einduction" induction_clause_list
| "destruct" induction_clause_list
| "edestruct" induction_clause_list
| "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
| "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" constr ]
| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list
| "inversion" quantified_hypothesis "using" constr in_hyp_list
| "red" clause_dft_concl
| "hnf" clause_dft_concl
| "simpl" OPT "head" delta_flag OPT ref_or_pattern_occ clause_dft_concl
| "cbv" strategy_flag clause_dft_concl
| "cbn" strategy_flag clause_dft_concl
| "lazy" strategy_flag clause_dft_concl
| "compute" delta_flag clause_dft_concl
| "vm_compute" OPT ref_or_pattern_occ clause_dft_concl
| "native_compute" OPT ref_or_pattern_occ clause_dft_concl
| "unfold" LIST1 unfold_occ SEP "," clause_dft_concl
| "fold" LIST1 constr clause_dft_concl
| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl
| "change" conversion clause_dft_concl
| "change_no_check" conversion clause_dft_concl
| "start" "ltac" "profiling"
| "stop" "ltac" "profiling"
| "reset" "ltac" "profile"
| "show" "ltac" "profile"
| "show" "ltac" "profile" "cutoff" integer
| "show" "ltac" "profile" string
| "restart_timer" OPT string
| "finish_timing" OPT string
| "finish_timing" "(" string ")" OPT string
| "xlra_Q" tactic      (* micromega plugin *)
| "wlra_Q" ident constr      (* micromega plugin *)
| "xlra_R" tactic      (* micromega plugin *)
| "xlia" tactic      (* micromega plugin *)
| "wlia" ident constr      (* micromega plugin *)
| "xnra_Q" tactic      (* micromega plugin *)
| "wnra_Q" ident constr      (* micromega plugin *)
| "xnra_R" tactic      (* micromega plugin *)
| "xnia" tactic      (* micromega plugin *)
| "wnia" ident constr      (* micromega plugin *)
| "xsos_Z" tactic      (* micromega plugin *)
| "wsos_Z" ident constr      (* micromega plugin *)
| "xsos_Q" tactic      (* micromega plugin *)
| "wsos_Q" ident constr      (* micromega plugin *)
| "xsos_R" tactic      (* micromega plugin *)
| "xpsatz_Z" nat_or_var tactic      (* micromega plugin *)
| "wpsatz_Z" nat_or_var ident constr      (* micromega plugin *)
| "xpsatz_Q" nat_or_var tactic      (* micromega plugin *)
| "wpsatz_Q" nat_or_var ident constr      (* micromega plugin *)
| "xpsatz_R" nat_or_var tactic      (* micromega plugin *)
| "zify_iter_specs"      (* micromega plugin *)
| "zify_op"      (* micromega plugin *)
| "zify_saturate"      (* micromega plugin *)
| "zify_iter_let" tactic      (* micromega plugin *)
| "zify_elim_let"      (* micromega plugin *)
| "nsatz_compute" constr      (* nsatz plugin *)
| "protect_fv" string "in" ident      (* ring plugin *)
| "protect_fv" string      (* ring plugin *)
| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
| "rtauto"
]

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

int_or_id: [
| preident      (* extraction plugin *)
| integer      (* extraction plugin *)
]

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

firstorder_using: [
| "using" LIST1 reference SEP ","
|
]

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

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

function_fix_definition: [
| Vernac.fix_definition      (* funind plugin *)
]

fun_scheme_arg: [
| identref ":=" "Induction" "for" reference "Sort" sort_quality_or_set      (* funind plugin *)
]

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

EXTRAARGS_natural: [
| _natural
]

occurrences: [
| LIST1 integer
| hyp
]

glob: [
| constr
]

EXTRAARGS_lconstr: [
| l_constr
]

lglob: [
| EXTRAARGS_lconstr
]

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

rename: [
| ident "into" ident
]

by_arg_tac: [
| "by" tactic3
|
]

in_clause: [
| in_clause'
| "*" occs
| "*" "|-" concl_occ
| "|-" concl_occ
| LIST1 hypident_occ SEP "," "|-" concl_occ
| LIST1 hypident_occ SEP ","
]

test_lpar_id_colon: [
| local_test_lpar_id_colon
]

EXTRAARGS_strategy_level: [
| strategy_level0
]

strategy_level_or_var: [
| EXTRAARGS_strategy_level
| identref
]

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

test: [
| int_or_var comparison int_or_var
]

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

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

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

opthints: [
| ":" LIST1 preident
|
]

debug: [
| "debug"
|
]

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

eauto_search_strategy: [
| "(" eauto_search_strategy_name ")"
|
]

tactic_then_last: [
| "|" LIST0 ( OPT ltac_expr5 ) SEP "|"
|
]

for_each_goal: [
| ltac_expr5 "|" for_each_goal
| ltac_expr5 ".." tactic_then_last
| ".." tactic_then_last
| ltac_expr5
| "|" for_each_goal
|
]

tactic_then_locality: [
| "[" OPT ">"
]

ltac_expr5: [
| ltac_expr4
]

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

ltac_expr3: [
| "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
| "abstract" ltac_expr2 "using" ident
| "only" goal_selector ":" ltac_expr3
| ltac_expr2
]

ltac_expr2: [
| ltac_expr1 "+" ltac_expr2
| "tryif" ltac_expr5 "then" ltac_expr5 "else" ltac_expr2
| ltac_expr1 "||" ltac_expr2
| ltac_expr1
]

ltac_expr1: [
| "fun" LIST1 input_fun "=>" ltac_expr5
| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
| match_key "goal" "with" match_context_list "end"
| match_key "reverse" "goal" "with" match_context_list "end"
| match_key ltac_expr5 "with" match_list "end"
| "first" "[" LIST0 ltac_expr5 SEP "|" "]"
| "solve" "[" LIST0 ltac_expr5 SEP "|" "]"
| "idtac" LIST0 message_token
| failkw [ nat_or_var | ] LIST0 message_token
| simple_tactic
| tactic_value
| reference LIST0 tactic_arg
| ltac_expr0
]

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

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

tactic_arg: [
| tactic_value
| Constr.constr
| "()"
]

tactic_value: [
| constr_eval
| "fresh" LIST0 fresh_id
| "type_term" uconstr
| "numgoals"
]

fresh_id: [
| STRING
| qualid
]

constr_eval: [
| "eval" red_expr "in" Constr.constr
| "context" identref "[" Constr.lconstr "]"
| "type" "of" Constr.constr
]

tactic_atom: [
| integer
| reference
| "()"
]

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

input_fun: [
| "_"
| ident
]

let_clause: [
| identref ":=" ltac_expr5
| "_" ":=" ltac_expr5
| identref LIST1 input_fun ":=" ltac_expr5
]

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

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

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

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

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

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

message_token: [
| identref
| STRING
| natural
]

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

tacdef_body: [
| Constr.global LIST1 input_fun ltac_def_kind ltac_expr5
| Constr.global ltac_def_kind ltac_expr5
]

tactic: [
| ltac_expr5
]

tactic_mode: [
| subprf
| OPT toplevel_selector subprf_with_selector
| OPT ltac_selector OPT ltac_info tactic ltac_use_default
| "par" ":" OPT ltac_info tactic ltac_use_default
]

ltac_selector: [
| toplevel_selector
]

ltac_info: [
| "Info" natural
]

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

ltac_tactic_level: [
| "(" "at" "level" natural ")"
]

ltac_production_sep: [
| "," string
]

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

ltac_tacdef_body: [
| tacdef_body
]

glob_constr_with_bindings: [
| constr_with_bindings
]

rewstrategy: [
| "fix" identref ":=" rewstrategy1
| ne_rewstrategy1_list_sep_semicolon
]

ne_rewstrategy1_list_sep_semicolon: [
| ne_rewstrategy1_list_sep_semicolon ";" rewstrategy1
| rewstrategy1
]

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

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

id_or_meta: [
| identref
]

open_constr: [
| constr
]

uconstr: [
| constr
]

destruction_arg: [
| natural
| test_lpar_id_rpar constr_with_bindings
| constr_with_bindings_arg
]

constr_with_bindings_arg: [
| constr_with_bindings
]

quantified_hypothesis: [
| ident
| natural
]

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

intropatterns: [
| LIST0 intropattern
]

ne_intropatterns: [
| LIST1 intropattern
]

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

equality_intropattern: [
| "->"
| "<-"
| test_leftsquarebracket_equal "[" "=" intropatterns "]"
]

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

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

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

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

simple_binding: [
| "(" identref ":=" lconstr ")"
| "(" natural ":=" lconstr ")"
]

bindings: [
| test_lpar_idnum_coloneq LIST1 simple_binding
| LIST1 constr
]

constr_with_bindings: [
| constr with_bindings
]

with_bindings: [
| "with" bindings
|
]

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

hypident_occ: [
| hypident occs
]

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

clause_dft_all: [
| "in" in_clause
|
]

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

concl_occ: [
| "*" occs
|
]

in_hyp_list: [
| "in" LIST1 id_or_meta
|
]

in_hyp_as: [
| "in" LIST1 [ id_or_meta as_ipat ] SEP ","
|
]

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

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

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

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

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

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

eliminator: [
| "using" constr_with_bindings
]

as_ipat: [
| "as" simple_intropattern
|
]

or_and_intropattern_loc: [
| or_and_intropattern
| identref
]

as_or_and_ipat: [
| "as" equality_intropattern
| "as" or_and_intropattern_loc
|
]

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

as_name: [
| "as" ident
|
]

by_tactic: [
| "by" ltac_expr3
|
]

rewriter: [
| "!" constr_with_bindings_arg
| [ "?" | LEFTQMARK ] constr_with_bindings_arg
| natural "!" constr_with_bindings_arg
| natural [ "?" | LEFTQMARK ] constr_with_bindings_arg
| natural constr_with_bindings_arg
| constr_with_bindings_arg
]

oriented_rewriter: [
| orient_rw rewriter
]

induction_clause: [
| destruction_arg as_or_and_ipat eqn_ipat opt_clause
]

induction_clause_list: [
| LIST1 induction_clause SEP "," OPT eliminator opt_clause
]

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

ring_mods: [
| "(" LIST1 ring_mod SEP "," ")"      (* ring plugin *)
]

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

field_mods: [
| "(" LIST1 field_mod SEP "," ")"      (* ring plugin *)
]

number_string_mapping: [
| reference "=>" reference
| "[" reference "]" "=>" reference
]

number_string_via: [
| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]"
]

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

number_options: [
| "(" LIST1 number_modifier SEP "," ")"
]

string_option: [
| "(" number_string_via ")"
]

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

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

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

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

ltac2_expr5: [
| "fun" LIST1 G_LTAC2_input_fun type_cast "=>" ltac2_expr6      (* ltac2 plugin *)
| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6      (* ltac2 plugin *)
| "match" ltac2_expr5 "with" G_LTAC2_branches "end"      (* ltac2 plugin *)
| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5      (* ltac2 plugin *)
| ltac2_expr4      (* ltac2 plugin *)
]

ltac2_expr4: [
| ltac2_expr3      (* ltac2 plugin *)
]

ltac2_expr3: [
| ltac2_expr2 "," LIST1 ltac2_expr2 SEP ","      (* ltac2 plugin *)
| ltac2_expr2      (* 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 ".(" Prim.qualid ")"      (* ltac2 plugin *)
| ltac2_expr0 ".(" Prim.qualid ")" ":=" ltac2_expr5      (* ltac2 plugin *)
| ltac2_expr0      (* ltac2 plugin *)
]

ltac2_expr0: [
| "(" ltac2_expr6 ")"      (* ltac2 plugin *)
| "(" ltac2_expr6 ":" ltac2_type5 ")"      (* ltac2 plugin *)
| "()"      (* ltac2 plugin *)
| "(" ")"      (* ltac2 plugin *)
| array_literal      (* ltac2 plugin *)
| list_literal      (* ltac2 plugin *)
| "{" test_qualid_with_or_lpar_or_rbrac ltac2_expr0 "with" tac2rec_fieldexprs "}"      (* ltac2 plugin *)
| "{" tac2rec_fieldexprs "}"      (* ltac2 plugin *)
| ltac2_atom      (* ltac2 plugin *)
]

array_literal: [
| test_array_opening "[" "|" LIST0 ltac2_expr5 SEP ";" test_array_closing "|" "]"      (* ltac2 plugin *)
]

list_literal: [
| "[" LIST0 ltac2_expr5 SEP ";" "]"      (* ltac2 plugin *)
]

G_LTAC2_branches: [
|      (* ltac2 plugin *)
| "|" LIST1 branch SEP "|"      (* ltac2 plugin *)
| LIST1 branch SEP "|"      (* ltac2 plugin *)
]

branch: [
| atomic_tac2pat "=>" ltac2_expr6      (* ltac2 plugin *)
]

rec_flag: [
| "rec"      (* ltac2 plugin *)
|      (* ltac2 plugin *)
]

mut_flag: [
| "mutable"      (* ltac2 plugin *)
|      (* ltac2 plugin *)
]

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

ltac2_atom: [
| Prim.integer      (* ltac2 plugin *)
| Prim.string      (* ltac2 plugin *)
| Prim.qualid      (* ltac2 plugin *)
| "@" Prim.ident      (* ltac2 plugin *)
| "&" identref      (* ltac2 plugin *)
| "'" Constr.constr      (* ltac2 plugin *)
| "constr" ":" "(" Constr.lconstr ")"      (* ltac2 plugin *)
| "open_constr" ":" "(" Constr.lconstr ")"      (* ltac2 plugin *)
| "preterm" ":" "(" Constr.lconstr ")"      (* ltac2 plugin *)
| "ident" ":" "(" identref ")"      (* ltac2 plugin *)
| "pat" ":" "(" Constr.cpattern ")"      (* ltac2 plugin *)
| "reference" ":" "(" globref ")"      (* ltac2 plugin *)
| "ltac1" ":" "(" ltac1_expr_in_env ")"      (* ltac2_ltac1 plugin *)
| "ltac1val" ":" "(" ltac1_expr_in_env ")"      (* ltac2_ltac1 plugin *)
]

tac2expr_in_env: [
| test_ltac1_env LIST0 identref "|-" ltac2_expr6      (* ltac2 plugin *)
| ltac2_expr6      (* ltac2 plugin *)
]

type_cast: [
|      (* ltac2 plugin *)
| ":" ltac2_type5      (* ltac2 plugin *)
]

G_LTAC2_let_clause: [
| let_binder type_cast ":=" ltac2_expr6      (* ltac2 plugin *)
]

let_binder: [
| LIST1 G_LTAC2_input_fun      (* ltac2 plugin *)
]

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

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

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

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

G_LTAC2_binder: [
| "_"      (* ltac2 plugin *)
| Prim.ident      (* ltac2 plugin *)
]

G_LTAC2_input_fun: [
| tac2pat0      (* ltac2 plugin *)
]

tac2def_body: [
| G_LTAC2_binder LIST0 G_LTAC2_input_fun type_cast ":=" ltac2_expr6      (* ltac2 plugin *)
]

tac2def_val: [
| mut_flag rec_flag LIST1 tac2def_body SEP "with"      (* ltac2 plugin *)
]

tac2def_mut: [
| "Set" Prim.qualid OPT [ "as" identref ] ":=" ltac2_expr6      (* ltac2 plugin *)
]

tac2typ_knd: [
| ltac2_type5      (* ltac2 plugin *)
| "[" ".." "]"      (* ltac2 plugin *)
| "[" tac2alg_constructors "]"      (* ltac2 plugin *)
| "{" tac2rec_fields "}"      (* ltac2 plugin *)
]

tac2alg_constructors: [
| "|" LIST1 tac2alg_constructor SEP "|"      (* ltac2 plugin *)
| LIST0 tac2alg_constructor SEP "|"      (* ltac2 plugin *)
]

tac2alg_constructor: [
| quoted_attributes Prim.ident      (* ltac2 plugin *)
| quoted_attributes Prim.ident "(" LIST0 ltac2_type5 SEP "," ")"      (* ltac2 plugin *)
]

tac2rec_fields: [
| tac2rec_field ";" tac2rec_fields      (* ltac2 plugin *)
| tac2rec_field ";"      (* ltac2 plugin *)
| tac2rec_field      (* ltac2 plugin *)
|      (* ltac2 plugin *)
]

tac2rec_field: [
| mut_flag Prim.ident ":" ltac2_type5      (* ltac2 plugin *)
]

tac2rec_fieldexprs: [
| tac2rec_fieldexpr ";" tac2rec_fieldexprs      (* ltac2 plugin *)
| tac2rec_fieldexpr ";"      (* ltac2 plugin *)
| tac2rec_fieldexpr      (* ltac2 plugin *)
|      (* ltac2 plugin *)
]

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

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

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

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

tac2typ_def: [
| tac2typ_prm Prim.qualid tac2type_body      (* ltac2 plugin *)
]

tac2type_body: [
|      (* ltac2 plugin *)
| ":=" tac2typ_knd      (* ltac2 plugin *)
| "::=" tac2typ_knd      (* ltac2 plugin *)
]

tac2def_typ: [
| "Type" rec_flag LIST1 tac2typ_def SEP "with"      (* ltac2 plugin *)
]

tac2def_ext: [
| "@" "external" identref ":" ltac2_type5 ":=" Prim.string Prim.string      (* ltac2 plugin *)
]

syn_node: [
| "_"      (* ltac2 plugin *)
| Prim.ident      (* ltac2 plugin *)
]

ltac2_syntax_class: [
| Prim.string      (* ltac2 plugin *)
| Prim.integer      (* ltac2 plugin *)
| syn_node      (* ltac2 plugin *)
| syn_node "(" LIST1 ltac2_syntax_class SEP "," ")"      (* ltac2 plugin *)
]

syn_level: [
|      (* ltac2 plugin *)
| ":" Prim.natural      (* ltac2 plugin *)
]

tac2def_syn: [
| LIST1 ltac2_syntax_class syn_level ":=" ltac2_expr6      (* ltac2 plugin *)
]

globref: [
| "&" Prim.ident      (* ltac2 plugin *)
| Prim.qualid      (* ltac2 plugin *)
]

anti: [
| "$" Prim.ident      (* ltac2 plugin *)
]

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

lnatural: [
| Prim.natural      (* ltac2 plugin *)
]

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

qhyp: [
| anti      (* ltac2 plugin *)
| lnatural      (* ltac2 plugin *)
| identref      (* ltac2 plugin *)
]

G_LTAC2_simple_binding: [
| "(" qhyp ":=" Constr.lconstr ")"      (* ltac2 plugin *)
]

G_LTAC2_bindings: [
| test_lpar_idnum_coloneq LIST1 G_LTAC2_simple_binding      (* ltac2 plugin *)
| LIST1 Constr.constr      (* ltac2 plugin *)
]

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

q_with_bindings: [
| G_LTAC2_with_bindings      (* ltac2 plugin *)
]

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

G_LTAC2_or_and_intropattern: [
| "[" LIST1 G_LTAC2_intropatterns SEP "|" "]"      (* ltac2 plugin *)
| "()"      (* ltac2 plugin *)
| "(" G_LTAC2_simple_intropattern ")"      (* ltac2 plugin *)
| "(" G_LTAC2_simple_intropattern "," LIST1 G_LTAC2_simple_intropattern SEP "," ")"      (* ltac2 plugin *)
| "(" G_LTAC2_simple_intropattern "&" LIST1 G_LTAC2_simple_intropattern SEP "&" ")"      (* ltac2 plugin *)
]

G_LTAC2_equality_intropattern: [
| "->"      (* ltac2 plugin *)
| "<-"      (* ltac2 plugin *)
| test_leftsquarebracket_equal "[" "=" G_LTAC2_intropatterns "]"      (* ltac2 plugin *)
]

G_LTAC2_naming_intropattern: [
| LEFTQMARK identref      (* ltac2 plugin *)
| "?$" identref      (* ltac2 plugin *)
| "?"      (* ltac2 plugin *)
| ident_or_anti      (* ltac2 plugin *)
]

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

G_LTAC2_simple_intropattern: [
| G_LTAC2_simple_intropattern_closed LIST0 [ "%" Constr.term0 ]      (* ltac2 plugin *)
]

G_LTAC2_simple_intropattern_closed: [
| G_LTAC2_or_and_intropattern      (* ltac2 plugin *)
| G_LTAC2_equality_intropattern      (* ltac2 plugin *)
| "_"      (* ltac2 plugin *)
--> --------------------

--> maximum size reached

--> --------------------