path: root/doc/tools/docgram/orderedGrammar

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

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

removed_opt: [
| "removed"
| empty
]

tactic_mode: [
| toplevel_selector_opt query_command
| toplevel_selector_opt "{"
| toplevel_selector_opt ltac_info_opt ltac_expr ltac_use_default
| "par" ":" ltac_info_opt ltac_expr ltac_use_default
]

toplevel_selector_opt: [
| toplevel_selector
| empty
]

ltac_info_opt: [
| "Info" num
| empty
]

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

vernac_control: [
| "Time" vernac_control
| "Redirect" string vernac_control
| "Timeout" num vernac_control
| "Fail" vernac_control
| quoted_attributes_list_opt vernac
]

term: [
| "forall" open_binders "," term
| "fun" open_binders "=>" term
| term_let
| "if" term as_return_type_opt "then" term "else" term
| term_fix
| term100
]

term100: [
| term_cast
| term10
]

term10: [
| term1 args
| "@" qualid universe_annot_opt term1_list_opt
| term1
]

args: [
| args arg
| arg
]

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

term1_list_opt: [
| term1_list_opt term1
| empty
]

empty: [
|
]

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

args_opt: [
| args
| empty
]

term0: [
| qualid universe_annot_opt
| sort
| numeral
| string
| "_"
| term_evar
| term_match
| "(" term ")"
| "{|" fields_def "|}"
| "`{" term "}"
| "`(" term ")"
| "ltac" ":" "(" ltac_expr ")"
]

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

field_def: [
| qualid binders_opt ":=" term
]

binders_opt: [
| binders
| empty
]

term_projection: [
| term0 ".(" qualid args_opt ")"
| term0 ".(" "@" qualid term1_list_opt ")"
]

term_evar: [
| "?[" ident "]"
| "?[" "?" ident "]"
| "?" ident evar_bindings_opt
]

evar_bindings_opt: [
| "@{" evar_bindings_semi "}"
| empty
]

evar_bindings_semi: [
| evar_bindings_semi ";" evar_binding
| evar_binding
]

evar_binding: [
| ident ":=" term
]

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

ident_list: [
| ident_list ident
| ident
]

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

record_field: [
| quoted_attributes_list_opt record_binder num_opt2 decl_notation
]

decl_notation: [
| "where" one_decl_notation_list
| empty
]

one_decl_notation_list: [
| one_decl_notation_list "and" one_decl_notation
| one_decl_notation
]

one_decl_notation: [
| string ":=" term1_extended ident_opt3
]

ident_opt3: [
| ":" ident
| empty
]

record_binder: [
| name
| name record_binder_body
]

record_binder_body: [
| binders_opt of_type_with_opt_coercion term
| binders_opt of_type_with_opt_coercion term ":=" term
| binders_opt ":=" term
]

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

num_opt2: [
| "|" num
| empty
]

quoted_attributes_list_opt: [
| quoted_attributes_list_opt "#[" attribute_list_comma_opt "]"
| empty
]

attribute_list_comma_opt: [
| attribute_list_comma
| empty
]

attribute_list_comma: [
| attribute_list_comma "," attribute
| attribute
]

attribute: [
| ident attribute_value
]

attribute_value: [
| "=" string
| "(" attribute_list_comma_opt ")"
| empty
]

qualid: [
| qualid field
| ident
]

field: [
| "." ident
]

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

universe: [
| "max" "(" universe_exprs_comma ")"
| universe_expr
]

universe_exprs_comma: [
| universe_exprs_comma "," universe_expr
| universe_expr
]

universe_expr: [
| universe_name universe_increment_opt
]

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

universe_increment_opt: [
| "+" num
| empty
]

universe_annot_opt: [
| "@{" universe_levels_opt "}"
| empty
]

universe_levels_opt: [
| universe_levels_opt universe_level
| empty
]

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

term_fix: [
| single_fix
| single_fix "with" fix_bodies "for" ident
]

single_fix: [
| "fix" fix_body
| "cofix" fix_body
]

fix_bodies: [
| fix_bodies "with" fix_body
| fix_body
]

fix_body: [
| ident binders_opt fixannot_opt colon_term_opt ":=" term
]

fixannot_opt: [
| fixannot
| empty
]

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

term1_extended: [
| term1
| "@" qualid universe_annot_opt
]

ident_opt: [
| ident
| empty
]

term1_extended_opt: [
| term1_extended
| empty
]

term_let: [
| "let" name colon_term_opt ":=" term "in" term
| "let" name binders colon_term_opt ":=" term "in" term
| "let" single_fix "in" term
| "let" names_tuple as_return_type_opt ":=" term "in" term
| "let" "'" pattern ":=" term return_type_opt "in" term
| "let" "'" pattern "in" pattern ":=" term return_type "in" term
]

colon_term_opt: [
| ":" term
| empty
]

names_tuple: [
| "(" names_comma ")"
| "()"
]

names_comma: [
| names_comma "," name
| name
]

open_binders: [
| names ":" term
| binders
]

names: [
| names name
| name
]

name: [
| "_"
| ident
]

binders: [
| binders binder
| binder
]

binder: [
| name
| "(" names ":" term ")"
| "(" name colon_term_opt ":=" term ")"
| "{" name "}"
| "{" names colon_term_opt "}"
| "`(" typeclass_constraints_comma ")"
| "`{" typeclass_constraints_comma "}"
| "'" pattern0
| "(" name ":" term "|" term ")"
]

typeclass_constraints_comma: [
| typeclass_constraints_comma "," typeclass_constraint
| typeclass_constraint
]

typeclass_constraint: [
| exclam_opt term
| "{" name "}" ":" exclam_opt term
| name ":" exclam_opt term
]

exclam_opt: [
| "!"
| empty
]

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

term_match: [
| "match" case_items_comma return_type_opt "with" or_opt eqns_or_opt "end"
]

case_items_comma: [
| case_items_comma "," case_item
| case_item
]

return_type_opt: [
| return_type
| empty
]

as_return_type_opt: [
| as_name_opt return_type
| empty
]

return_type: [
| "return" term100
]

case_item: [
| term100 as_name_opt in_opt
]

as_name_opt: [
| "as" name
| empty
]

in_opt: [
| "in" pattern
| empty
]

or_opt: [
| "|"
| empty
]

eqns_or_opt: [
| eqns_or
| empty
]

eqns_or: [
| eqns_or "|" eqn
| eqn
]

eqn: [
| patterns_comma_list_or "=>" term
]

patterns_comma_list_or: [
| patterns_comma_list_or "|" patterns_comma
| patterns_comma
]

patterns_comma: [
| patterns_comma "," pattern
| pattern
]

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

pattern10: [
| pattern1 "as" name
| pattern1_list
| "@" qualid pattern1_list_opt
| pattern1
]

pattern1_list: [
| pattern1_list pattern1
| pattern1
]

pattern1_list_opt: [
| pattern1_list
| empty
]

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

pattern0: [
| qualid
| "{|" record_patterns_opt "|}"
| "_"
| "(" patterns_or ")"
| numeral
| string
]

patterns_or: [
| patterns_or "|" pattern
| pattern
]

record_patterns_opt: [
| record_patterns_opt ";" record_pattern
| record_pattern
| empty
]

record_pattern: [
| qualid ":=" pattern
]

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

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

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

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

gallina: [
| thm_token ident_decl binders_opt ":" term with_list_opt
| assumption_token inline assum_list
| assumptions_token inline assum_list
| def_token ident_decl def_body
| "Let" ident def_body
| cumulativity_token_opt private_token finite_token inductive_definition_list
| "Fixpoint" fix_definition_list
| "Let" "Fixpoint" fix_definition_list
| "CoFixpoint" cofix_definition_list
| "Let" "CoFixpoint" cofix_definition_list
| "Scheme" scheme_list
| "Combined" "Scheme" ident "from" ident_list_comma
| "Register" qualid "as" qualid
| "Register" "Inline" qualid
| "Primitive" ident term_opt ":=" register_token
| "Universe" ident_list
| "Universes" ident_list
| "Constraint" univ_constraint_list_comma
]

term_opt: [
| ":" term
| empty
]

univ_constraint_list_comma: [
| univ_constraint_list_comma "," univ_constraint
| univ_constraint
]

with_list_opt: [
| with_list_opt "with" ident_decl binders_opt ":" term
| empty
]

cumulativity_token_opt: [
| cumulativity_token
| empty
]

inductive_definition_list: [
| inductive_definition_list "with" inductive_definition
| inductive_definition
]

fix_definition_list: [
| fix_definition_list "with" fix_definition
| fix_definition
]

fix_definition: [
| ident_decl binders_opt fixannot_opt colon_term_opt term_opt2 decl_notation
]

term_opt2: [
| ":=" term
| empty
]

cofix_definition_list: [
| cofix_definition_list "with" cofix_definition
| cofix_definition
]

scheme_list: [
| scheme_list "with" scheme
| scheme
]

ident_list_comma: [
| ident_list_comma "," ident
| ident
]

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

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

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

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

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

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

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

univ_constraint: [
| universe_name lt_alt universe_name
]

lt_alt: [
| "<"
| "="
| "<="
]

ident_decl: [
| ident univ_decl_opt
]

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

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

private_token: [
| "Private"
| empty
]

def_body: [
| binders_opt ":=" reduce term
| binders_opt ":" term ":=" reduce term
| binders_opt ":" term
]

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

red_expr: [
| "red"
| "hnf"
| "simpl" delta_flag ref_or_pattern_occ_opt
| "cbv" strategy_flag
| "cbn" strategy_flag
| "lazy" strategy_flag
| "compute" delta_flag
| "vm_compute" ref_or_pattern_occ_opt
| "native_compute" ref_or_pattern_occ_opt
| "unfold" unfold_occ_list_comma
| "fold" term1_extended_list
| "pattern" pattern_occ_list_comma
| ident
]

strategy_flag: [
| red_flags_list
| delta_flag
]

red_flags_list: [
| red_flags_list red_flags
| red_flags
]

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

delta_flag: [
| "-" "[" smart_global_list "]"
| "[" smart_global_list "]"
| empty
]

ref_or_pattern_occ_opt: [
| ref_or_pattern_occ
| empty
]

ref_or_pattern_occ: [
| smart_global occs
| term1_extended occs
]

unfold_occ_list_comma: [
| unfold_occ_list_comma "," unfold_occ
| unfold_occ
]

unfold_occ: [
| smart_global occs
]

pattern_occ_list_comma: [
| pattern_occ_list_comma "," pattern_occ
| pattern_occ
]

opt_constructors_or_fields: [
| ":=" constructor_list_or_record_decl
| empty
]

inductive_definition: [
| opt_coercion ident_decl binders_opt term_opt opt_constructors_or_fields decl_notation
]

opt_coercion: [
| ">"
| empty
]

constructor_list_or_record_decl: [
| "|" constructor_list_or
| ident constructor_type "|" constructor_list_or_opt
| ident constructor_type
| ident "{" record_fields "}"
| "{" record_fields "}"
| empty
]

constructor_list_or: [
| constructor_list_or "|" constructor
| constructor
]

constructor_list_or_opt: [
| constructor_list_or
| empty
]

assum_list: [
| assum_coe_list
| simple_assum_coe
]

assum_coe_list: [
| assum_coe_list assum_coe
| assum_coe
]

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

simple_assum_coe: [
| ident_decl_list of_type_with_opt_coercion term
]

ident_decl_list: [
| ident_decl_list ident_decl
| ident_decl
]

constructor_type: [
| binders_opt of_type_with_opt_coercion_opt
]

of_type_with_opt_coercion_opt: [
| of_type_with_opt_coercion term
| empty
]

constructor: [
| ident constructor_type
]

cofix_definition: [
| ident_decl binders_opt colon_term_opt term_opt2 decl_notation
]

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

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

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

smart_global: [
| qualid
| by_notation
]

by_notation: [
| string ident_opt2
]

ident_opt2: [
| "%" ident
| empty
]

gallina_ext: [
| "Module" export_token ident module_binder_list_opt of_module_type is_module_expr
| "Module" "Type" ident module_binder_list_opt module_type_inl_list_opt is_module_type
| "Declare" "Module" export_token ident module_binder_list_opt ":" module_type_inl
| "Section" ident
| "Chapter" ident
| "End" ident
| "Collection" ident ":=" section_subset_expr
| "Require" export_token qualid_list
| "From" qualid "Require" export_token qualid_list
| "Import" qualid_list
| "Export" qualid_list
| "Include" module_type_inl module_expr_inl_list_opt
| "Include" "Type" module_type_inl module_type_inl_list_opt
| "Transparent" smart_global_list
| "Opaque" smart_global_list
| "Strategy" strategy_level_list
| "Canonical" Structure_opt qualid univ_decl_opt2
| "Canonical" Structure_opt by_notation
| "Coercion" qualid univ_decl_opt def_body
| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr
| "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr
| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
| "Context" binders
| "Instance" instance_name ":" term hint_info fields_def_opt
| "Existing" "Instance" qualid hint_info
| "Existing" "Instances" qualid_list num_opt2
| "Existing" "Class" qualid
| "Arguments" smart_global argument_spec_block_list_opt more_implicits_block_opt arguments_modifier_opt
| "Implicit" "Type" reserv_list
| "Implicit" "Types" reserv_list
| "Generalizable" All_alt
| "Export" "Set" ident_list option_setting
| "Export" "Unset" ident_list
]

smart_global_list: [
| smart_global_list smart_global
| smart_global
]

num_opt: [
| num
| empty
]

qualid_list: [
| qualid_list qualid
| qualid
]

option_setting: [
| empty
| int
| string
]

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

hint_info: [
| "|" num_opt term1_extended_opt
| empty
]

module_binder_list_opt: [
| module_binder_list_opt "(" export_token ident_list ":" module_type_inl ")"
| empty
]

module_type_inl_list_opt: [
| module_type_inl_list_opt module_type_inl
| empty
]

module_expr_inl_list_opt: [
| module_expr_inl_list_opt module_expr_inl
| empty
]

strategy_level_list: [
| strategy_level_list strategy_level "[" smart_global_list "]"
| strategy_level "[" smart_global_list "]"
]

fields_def_opt: [
| ":=" "{" fields_def "}"
| ":=" term
| empty
]

argument_spec_block_list_opt: [
| argument_spec_block_list_opt argument_spec_block
| empty
]

more_implicits_block_opt: [
| "," more_implicits_block_list_comma
| empty
]

more_implicits_block_list_comma: [
| more_implicits_block_list_comma "," more_implicits_block_list_opt
| more_implicits_block_list_opt
]

arguments_modifier_opt: [
| ":" arguments_modifier_list_comma
| empty
]

arguments_modifier_list_comma: [
| arguments_modifier_list_comma "," arguments_modifier
| arguments_modifier
]

All_alt: [
| "All" "Variables"
| "No" "Variables"
| Variable_alt ident_list
]

Variable_alt: [
| "Variable"
| "Variables"
]

more_implicits_block_list_opt: [
| more_implicits_block_list_opt more_implicits_block
| empty
]

univ_decl_opt2: [
| univ_decl_opt def_body
| empty
]

univ_decl_opt: [
| "@{" ident_list_opt plus_opt univ_constraint_alt
| empty
]

plus_opt: [
| "+"
| empty
]

univ_constraint_alt: [
| "|" univ_constraint_list_comma_opt plus_opt "}"
| rbrace_alt
]

univ_constraint_list_comma_opt: [
| univ_constraint_list_comma
| empty
]

rbrace_alt: [
| "}"
| "|}"
]

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

of_module_type: [
| ":" module_type_inl
| module_type_inl_list_opt
]

is_module_type: [
| ":=" module_type_inl module_type_inl_list_opt
| empty
]

is_module_expr: [
| ":=" module_expr_inl module_expr_inl_list_opt
| empty
]

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

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

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

module_expr: [
| module_expr_atom
| module_expr module_expr_atom
]

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

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

with_declaration: [
| "Definition" qualid univ_decl_opt ":=" term
| "Module" qualid ":=" qualid
]

argument_spec_block: [
| exclam_opt name scope_delimiter_opt
| "/"
| "&"
| "(" scope_delimiter_list ")" scope_delimiter_opt
| "[" scope_delimiter_list "]" scope_delimiter_opt
| "{" scope_delimiter_list "}" scope_delimiter_opt
]

scope_delimiter_opt: [
| "%" ident
| empty
]

scope_delimiter_list: [
| scope_delimiter_list scope_delimiter_opt
| scope_delimiter_opt
]

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

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

instance_name: [
| ident_decl binders_opt
| empty
]

reserv_list: [
| reserv_tuple_list
| simple_reserv
]

reserv_tuple_list: [
| reserv_tuple_list reserv_tuple
| reserv_tuple
]

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

simple_reserv: [
| ident_list ":" term
]

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

Structure_opt: [
| "Structure"
| empty
]

command: [
| "Goal" term
| "Comments" comment_list_opt
| "Declare" "Instance" ident_decl binders_opt ":" term hint_info
| "Declare" "Scope" ident
| "Pwd"
| "Cd"
| "Cd" string
| "Load" Verbose_opt string_alt
| "Declare" "ML" "Module" string_list
| "Locate" locatable
| "Add" "LoadPath" string as_dirpath
| "Add" "Rec" "LoadPath" string as_dirpath
| "Remove" "LoadPath" string
| "AddPath" string "as" as_dirpath
| "AddRecPath" string "as" as_dirpath
| "DelPath" string
| "Type" term
| "Print" printable
| "Print" smart_global univ_name_list_opt
| "Print" "Module" "Type" qualid
| "Print" "Module" qualid
| "Print" "Namespace" dirpath
| "Inspect" num
| "Add" "ML" "Path" string
| "Add" "Rec" "ML" "Path" string
| "Set" ident_list option_setting
| "Unset" ident_list
| "Print" "Table" ident_list
| "Add" ident ident option_ref_value_list
| "Add" ident option_ref_value_list
| "Test" ident_list "for" option_ref_value_list
| "Test" ident_list
| "Remove" ident ident option_ref_value_list
| "Remove" ident option_ref_value_list
| "Write" "State" ident
| "Write" "State" string
| "Restore" "State" ident
| "Restore" "State" string
| "Reset" "Initial"
| "Reset" ident
| "Back"
| "Back" num
| "Debug" "On"
| "Debug" "Off"
| "Declare" "Reduction" ident ":=" red_expr
| "Declare" "Custom" "Entry" ident
| "Derive" ident "SuchThat" term1_extended "As" ident      (* derive plugin *)
| "Proof"
| "Proof" "Mode" string
| "Proof" term
| "Abort"
| "Abort" "All"
| "Abort" ident
| "Existential" num constr_body
| "Admitted"
| "Qed"
| "Save" ident
| "Defined"
| "Defined" ident
| "Restart"
| "Undo"
| "Undo" num
| "Undo" "To" num
| "Focus"
| "Focus" num
| "Unfocus"
| "Unfocused"
| "Show"
| "Show" num
| "Show" ident
| "Show" "Existentials"
| "Show" "Universes"
| "Show" "Conjectures"
| "Show" "Proof"
| "Show" "Intro"
| "Show" "Intros"
| "Show" "Match" qualid
| "Guarded"
| "Create" "HintDb" ident discriminated_opt
| "Remove" "Hints" qualid_list opt_hintbases
| "Hint" hint opt_hintbases
| "Obligation" int "of" ident ":" term withtac
| "Obligation" int "of" ident withtac
| "Obligation" int ":" term withtac
| "Obligation" int withtac
| "Next" "Obligation" "of" ident withtac
| "Next" "Obligation" withtac
| "Solve" "Obligation" int "of" ident "with" ltac_expr
| "Solve" "Obligation" int "with" ltac_expr
| "Solve" "Obligations" "of" ident "with" ltac_expr
| "Solve" "Obligations" "with" ltac_expr
| "Solve" "Obligations"
| "Solve" "All" "Obligations" "with" ltac_expr
| "Solve" "All" "Obligations"
| "Admit" "Obligations" "of" ident
| "Admit" "Obligations"
| "Obligation" "Tactic" ":=" ltac_expr
| "Show" "Obligation" "Tactic"
| "Obligations" "of" ident
| "Obligations"
| "Preterm" "of" ident
| "Preterm"
| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Relation" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "as" ident
| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Parametric" "Relation" binders_opt ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident
| "Add" "Setoid" term1_extended term1_extended term1_extended "as" ident
| "Add" "Parametric" "Setoid" binders_opt ":" term1_extended term1_extended term1_extended "as" ident
| "Add" "Morphism" term1_extended ":" ident
| "Declare" "Morphism" term1_extended ":" ident
| "Add" "Morphism" term1_extended "with" "signature" term "as" ident
| "Add" "Parametric" "Morphism" binders_opt ":" term1_extended "with" "signature" term "as" ident
| "Grab" "Existential" "Variables"
| "Unshelve"
| "Declare" "Equivalent" "Keys" term1_extended term1_extended
| "Print" "Equivalent" "Keys"
| "Optimize" "Proof"
| "Optimize" "Heap"
| "Reset" "Ltac" "Profile"
| "Show" "Ltac" "Profile"
| "Show" "Ltac" "Profile" "CutOff" int
| "Show" "Ltac" "Profile" string
| "Add" "InjTyp" term1_extended      (* micromega plugin *)
| "Add" "BinOp" term1_extended      (* micromega plugin *)
| "Add" "UnOp" term1_extended      (* micromega plugin *)
| "Add" "CstOp" term1_extended      (* micromega plugin *)
| "Add" "BinRel" term1_extended      (* micromega plugin *)
| "Add" "PropOp" term1_extended      (* micromega plugin *)
| "Add" "PropUOp" term1_extended      (* micromega plugin *)
| "Add" "Spec" term1_extended      (* micromega plugin *)
| "Add" "BinOpSpec" term1_extended      (* micromega plugin *)
| "Add" "UnOpSpec" term1_extended      (* micromega plugin *)
| "Add" "Saturate" term1_extended      (* micromega plugin *)
| "Show" "Zify" "InjTyp"      (* micromega plugin *)
| "Show" "Zify" "BinOp"      (* micromega plugin *)
| "Show" "Zify" "UnOp"      (* micromega plugin *)
| "Show" "Zify" "CstOp"      (* micromega plugin *)
| "Show" "Zify" "BinRel"      (* micromega plugin *)
| "Show" "Zify" "Spec"      (* micromega plugin *)
| "Add" "Ring" ident ":" term1_extended ring_mods_opt      (* setoid_ring plugin *)
| "Hint" "Cut" "[" hints_path "]" opthints
| "Typeclasses" "Transparent" qualid_list_opt
| "Typeclasses" "Opaque" qualid_list_opt
| "Typeclasses" "eauto" ":=" debug eauto_search_strategy int_opt
| "Print" "Rewrite" "HintDb" ident
| "Proof" "with" ltac_expr using_opt
| "Proof" "using" section_subset_expr with_opt
| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" ltac_expr
| "Print" "Ltac" qualid
| "Locate" "Ltac" qualid
| "Ltac" tacdef_body_list
| "Print" "Ltac" "Signatures"
| "Set" "Firstorder" "Solver" ltac_expr
| "Print" "Firstorder" "Solver"
| "Extraction" qualid      (* extraction plugin *)
| "Recursive" "Extraction" qualid_list      (* extraction plugin *)
| "Extraction" string qualid_list      (* extraction plugin *)
| "Extraction" "TestCompile" qualid_list      (* extraction plugin *)
| "Separate" "Extraction" qualid_list      (* extraction plugin *)
| "Extraction" "Library" ident      (* extraction plugin *)
| "Recursive" "Extraction" "Library" ident      (* extraction plugin *)
| "Extraction" "Language" language      (* extraction plugin *)
| "Extraction" "Inline" qualid_list      (* extraction plugin *)
| "Extraction" "NoInline" qualid_list      (* extraction plugin *)
| "Print" "Extraction" "Inline"      (* extraction plugin *)
| "Reset" "Extraction" "Inline"      (* extraction plugin *)
| "Extraction" "Implicit" qualid "[" int_or_id_list_opt "]"      (* extraction plugin *)
| "Extraction" "Blacklist" ident_list      (* extraction plugin *)
| "Print" "Extraction" "Blacklist"      (* extraction plugin *)
| "Reset" "Extraction" "Blacklist"      (* extraction plugin *)
| "Extract" "Constant" qualid string_list_opt "=>" mlname      (* extraction plugin *)
| "Extract" "Inlined" "Constant" qualid "=>" mlname      (* extraction plugin *)
| "Extract" "Inductive" qualid "=>" mlname "[" mlname_list_opt "]" string_opt      (* extraction plugin *)
| "Show" "Extraction"      (* extraction plugin *)
| "Function" fix_definition_list      (* funind plugin *)
| "Functional" "Scheme" fun_scheme_arg_list      (* funind plugin *)
| "Functional" "Case" fun_scheme_arg      (* funind plugin *)
| "Generate" "graph" "for" qualid      (* funind plugin *)
| "Hint" "Rewrite" orient term1_extended_list ":" ident_list_opt
| "Hint" "Rewrite" orient term1_extended_list "using" ltac_expr ":" ident_list_opt
| "Hint" "Rewrite" orient term1_extended_list
| "Hint" "Rewrite" orient term1_extended_list "using" ltac_expr
| "Derive" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
| "Derive" "Inversion_clear" ident "with" term1_extended
| "Derive" "Inversion" ident "with" term1_extended "Sort" sort_family
| "Derive" "Inversion" ident "with" term1_extended
| "Derive" "Dependent" "Inversion" ident "with" term1_extended "Sort" sort_family
| "Derive" "Dependent" "Inversion_clear" ident "with" term1_extended "Sort" sort_family
| "Declare" "Left" "Step" term1_extended
| "Declare" "Right" "Step" term1_extended
| "Print" "Rings"      (* setoid_ring plugin *)
| "Add" "Field" ident ":" term1_extended field_mods_opt      (* setoid_ring plugin *)
| "Print" "Fields"      (* setoid_ring plugin *)
| "Numeral" "Notation" qualid qualid qualid ":" ident numnotoption
| "String" "Notation" qualid qualid qualid ":" ident
]

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

string_opt: [
| string
| empty
]

qualid_list_opt: [
| qualid_list_opt qualid
| empty
]

univ_name_list_opt: [
| "@{" name_list_opt "}"
| empty
]

name_list_opt: [
| name_list_opt name
| empty
]

section_subset_expr: [
| starredidentref_list_opt
| ssexpr
]

ssexpr: [
| "-" ssexpr50
| ssexpr50
]

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

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

starredidentref_list_opt: [
| starredidentref_list_opt starredidentref
| empty
]

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

int_opt: [
| int
| empty
]

using_opt: [
| "using" section_subset_expr
| empty
]

with_opt: [
| "with" ltac_expr
| empty
]

ltac_tactic_level_opt: [
| "(" "at" "level" num ")"
| empty
]

ltac_production_item_list: [
| ltac_production_item_list ltac_production_item
| ltac_production_item
]

tacdef_body_list: [
| tacdef_body_list "with" tacdef_body
| tacdef_body
]

printable: [
| "Term" smart_global univ_name_list_opt
| "All"
| "Section" qualid
| "Grammar" ident
| "Custom" "Grammar" ident
| "LoadPath" dirpath_opt
| "Modules"
| "Libraries"
| "ML" "Path"
| "ML" "Modules"
| "Debug" "GC"
| "Graph"
| "Classes"
| "TypeClasses"
| "Instances" smart_global
| "Coercions"
| "Coercion" "Paths" class_rawexpr class_rawexpr
| "Canonical" "Projections"
| "Typing" "Flags"
| "Tables"
| "Options"
| "Hint"
| "Hint" smart_global
| "Hint" "*"
| "HintDb" ident
| "Scopes"
| "Scope" ident
| "Visibility" ident_opt
| "Implicit" smart_global
| Sorted_opt "Universes" printunivs_subgraph_opt string_opt
| "Assumptions" smart_global
| "Opaque" "Dependencies" smart_global
| "Transparent" "Dependencies" smart_global
| "All" "Dependencies" smart_global
| "Strategy" smart_global
| "Strategies"
| "Registered"
]

dirpath_opt: [
| dirpath
| empty
]

dirpath: [
| ident
| dirpath field
]

Sorted_opt: [
| "Sorted"
| empty
]

printunivs_subgraph_opt: [
| "Subgraph" "(" qualid_list_opt ")"
| empty
]

comment_list_opt: [
| comment_list_opt comment
| empty
]

Verbose_opt: [
| "Verbose"
| empty
]

string_alt: [
| string
| ident
]

string_list: [
| string_list string
| string
]

option_ref_value_list: [
| option_ref_value_list option_ref_value
| option_ref_value
]

discriminated_opt: [
| "discriminated"
| empty
]

string_list_opt: [
| string_list_opt string
| empty
]

mlname_list_opt: [
| mlname_list_opt mlname
| empty
]

fun_scheme_arg_list: [
| fun_scheme_arg_list "with" fun_scheme_arg
| fun_scheme_arg
]

term1_extended_list: [
| term1_extended_list term1_extended
| term1_extended
]

ring_mods_opt: [
| "(" ring_mod_list_comma ")"      (* setoid_ring plugin *)
| empty
]

field_mods_opt: [
| "(" field_mod_list_comma ")"      (* setoid_ring plugin *)
| empty
]

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

option_ref_value: [
| qualid
| string
]

as_dirpath: [
| "as" dirpath
| empty
]

comment: [
| term1_extended
| string
| num
]

reference_or_constr: [
| qualid
| term1_extended
]

hint: [
| "Resolve" reference_or_constr_list hint_info
| "Resolve" "->" qualid_list num_opt
| "Resolve" "<-" qualid_list num_opt
| "Immediate" reference_or_constr_list
| "Variables" "Transparent"
| "Variables" "Opaque"
| "Constants" "Transparent"
| "Constants" "Opaque"
| "Transparent" qualid_list
| "Opaque" qualid_list
| "Mode" qualid plus_list
| "Unfold" qualid_list
| "Constructors" qualid_list
| "Extern" num term1_extended_opt "=>" ltac_expr
]

reference_or_constr_list: [
| reference_or_constr_list reference_or_constr
| reference_or_constr
]

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

plus_list: [
| plus_list plus_alt
| plus_alt
]

plus_alt: [
| "+"
| "!"
| "-"
]

withtac: [
| "with" ltac_expr
| empty
]

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

tacdef_body: [
| qualid fun_var_list ltac_def_kind ltac_expr
| qualid ltac_def_kind ltac_expr
]

ltac_production_item: [
| string
| ident "(" ident ltac_production_sep_opt ")"
| ident
]

ltac_production_sep_opt: [
| "," string
| empty
]

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

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

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

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

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

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

ring_mod_list_comma: [
| ring_mod_list_comma "," ring_mod
| ring_mod
]

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

field_mod_list_comma: [
| field_mod_list_comma "," field_mod
| field_mod
]

debug: [
| "debug"
| empty
]

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

hints_path_atom: [
| qualid_list
| "_"
]

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

opthints: [
| ":" ident_list
| empty
]

opt_hintbases: [
| empty
| ":" ident_list
]

int_or_id_list_opt: [
| int_or_id_list_opt int_or_id
| empty
]

query_command: [
| "Eval" red_expr "in" term "."
| "Compute" term "."
| "Check" term "."
| "About" smart_global univ_name_list_opt "."
| "SearchHead" term1_extended in_or_out_modules "."
| "SearchPattern" term1_extended in_or_out_modules "."
| "SearchRewrite" term1_extended in_or_out_modules "."
| "Search" searchabout_query searchabout_queries "."
| "SearchAbout" searchabout_query searchabout_queries "."
| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "."
]

ne_in_or_out_modules: [
| "inside" qualid_list
| "outside" qualid_list
]

in_or_out_modules: [
| ne_in_or_out_modules
| empty
]

positive_search_mark: [
| "-"
| empty
]

searchabout_query: [
| positive_search_mark string scope_delimiter_opt
| positive_search_mark term1_extended
]

searchabout_queries: [
| ne_in_or_out_modules
| searchabout_query searchabout_queries
| empty
]

searchabout_query_list: [
| searchabout_query_list searchabout_query
| searchabout_query
]

syntax: [
| "Open" "Scope" ident
| "Close" "Scope" ident
| "Delimit" "Scope" ident "with" ident
| "Undelimit" "Scope" ident
| "Bind" "Scope" ident "with" class_rawexpr_list
| "Infix" string ":=" term1_extended syntax_modifier_opt ident_opt3
| "Notation" ident ident_list_opt ":=" term1_extended only_parsing
| "Notation" string ":=" term1_extended syntax_modifier_opt ident_opt3
| "Format" "Notation" string string string
| "Reserved" "Infix" string syntax_modifier_opt
| "Reserved" "Notation" string syntax_modifier_opt
]

class_rawexpr_list: [
| class_rawexpr_list class_rawexpr
| class_rawexpr
]

syntax_modifier_opt: [
| "(" syntax_modifier_list_comma ")"
| empty
]

syntax_modifier_list_comma: [
| syntax_modifier_list_comma "," syntax_modifier
| syntax_modifier
]

only_parsing: [
| "(" "only" "parsing" ")"
| "(" "compat" string ")"
| empty
]

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

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

syntax_extension_type: [
| "ident"
| "global"
| "bigint"
| "binder"
| "constr"
| "constr" level_opt constr_as_binder_kind_opt
| "pattern"
| "pattern" "at" "level" num
| "strict" "pattern"
| "strict" "pattern" "at" "level" num
| "closed" "binder"
| "custom" ident level_opt constr_as_binder_kind_opt
]

level_opt: [
| level
| empty
]

constr_as_binder_kind_opt: [
| constr_as_binder_kind
| empty
]

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

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

int_or_var: [
| int
| ident
]

constr_with_bindings_opt: [
| constr_with_bindings
| empty
]

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

rename: [
| ident "into" ident
]

by_arg_tac: [
| "by" ltac_expr3
| empty
]

in_clause: [
| in_clause
| "*" occs
| "*" "|-" concl_occ
| hypident_occ_list_comma_opt "|-" concl_occ
| hypident_occ_list_comma_opt
]

occs: [
| "at" occs_nums
| empty
]

hypident_occ_list_comma_opt: [
| hypident_occ_list_comma
| empty
]

as_ipat: [
| "as" simple_intropattern
| empty
]

or_and_intropattern_loc: [
| or_and_intropattern
| ident
]

as_or_and_ipat: [
| "as" or_and_intropattern_loc
| empty
]

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

as_name: [
| "as" ident
| empty
]

by_tactic: [
| "by" ltac_expr3
| empty
]

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

qmark_alt: [
| "?"
| "?"
]

oriented_rewriter: [
| orient rewriter
]

induction_clause: [
| destruction_arg as_or_and_ipat eqn_ipat opt_clause
]

induction_clause_list: [
| induction_clause_list_comma eliminator_opt opt_clause
]

induction_clause_list_comma: [
| induction_clause_list_comma "," induction_clause
| induction_clause
]

eliminator_opt: [
| "using" constr_with_bindings
| empty
]

auto_using: [
| "using" term1_extended_list_comma
| empty
]

term1_extended_list_comma: [
| term1_extended_list_comma "," term1_extended
| term1_extended
]

intropattern_list_opt: [
| intropattern_list_opt intropattern
| empty
]

or_and_intropattern: [
| "[" intropattern_or_list_or "]"
| "(" simple_intropattern_list_comma_opt ")"
| "(" simple_intropattern "&" simple_intropattern_list_ ")"
]

simple_intropattern_list_comma_opt: [
| simple_intropattern_list_comma
| empty
]

simple_intropattern_list_comma: [
| simple_intropattern_list_comma "," simple_intropattern
| simple_intropattern
]

simple_intropattern_list_: [
| simple_intropattern_list_ "&" simple_intropattern
| simple_intropattern
]

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

simple_intropattern_list_opt: [
| simple_intropattern_list_opt simple_intropattern
| empty
]

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

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

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

simple_intropattern: [
| simple_intropattern_closed term0_list_opt
]

term0_list_opt: [
| term0_list_opt "%" term0
| empty
]

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

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

bindings: [
| simple_binding_list
| term1_extended_list
]

simple_binding_list: [
| simple_binding_list simple_binding
| simple_binding
]

constr_with_bindings_arg_list_comma: [
| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg
| constr_with_bindings_arg
]

fixdecl_list: [
| fixdecl_list fixdecl
| fixdecl
]

cofixdecl_list: [
| cofixdecl_list cofixdecl
| cofixdecl
]

pattern_occ_list_opt: [
| pattern_occ_list_opt "," pattern_occ as_name
| empty
]

pattern_occ: [
| term1_extended occs
]

oriented_rewriter_list_comma: [
| oriented_rewriter_list_comma "," oriented_rewriter
| oriented_rewriter
]

simple_alt: [
| "simple" "inversion"
| "inversion"
| "inversion_clear"
]

with_opt2: [
| "with" term1_extended
| empty
]

bindings_list_comma: [
| bindings_list_comma "," bindings
| bindings
]

rename_list_comma: [
| rename_list_comma "," rename
| rename
]

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

hintbases: [
| "with" "*"
| "with" ident_list
| empty
]

qualid_opt: [
| qualid
| empty
]

bindings_with_parameters: [
| "(" ident simple_binder_list_opt ":=" term ")"
]

simple_binder_list_opt: [
| simple_binder_list_opt simple_binder
| empty
]

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

hypident_occ: [
| hypident occs
]

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

clause_dft_all: [
| "in" in_clause
| empty
]

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

occs_nums: [
| num_or_var_list
| "-" num_or_var int_or_var_list_opt
]

num_or_var: [
| num
| ident
]

int_or_var_list_opt: [
| int_or_var_list_opt int_or_var
| empty
]

num_or_var_list: [
| num_or_var_list num_or_var
| num_or_var
]

concl_occ: [
| "*" occs
| empty
]

in_hyp_list: [
| "in" ident_list
| empty
]

in_hyp_as: [
| "in" ident as_ipat
| empty
]

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

fixdecl: [
| "(" ident simple_binder_list_opt struct_annot ":" term ")"
]

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

cofixdecl: [
| "(" ident simple_binder_list_opt ":" term ")"
]

constr_with_bindings: [
| term1_extended with_bindings
]

with_bindings: [
| "with" bindings
| empty
]

destruction_arg: [
| num
| constr_with_bindings
| constr_with_bindings_arg
]

constr_with_bindings_arg: [
| ">" constr_with_bindings
| constr_with_bindings
]

quantified_hypothesis: [
| ident
| num
]

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

firstorder_using: [
| "using" qualid
| "using" qualid "," qualid_list_comma
| "using" qualid qualid qualid_list_opt
| empty
]

qualid_list_comma: [
| qualid_list_comma "," qualid
| qualid
]

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

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

occurrences: [
| int_list
| ident
]

int_list: [
| int_list int
| int
]

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

hypident_occ_list_comma: [
| hypident_occ_list_comma "," hypident_occ
| hypident_occ
]

ltac_expr: [
| binder_tactic
| ltac_expr4
]

binder_tactic: [
| "fun" fun_var_list "=>" ltac_expr
| "let" rec_opt let_clause_list "in" ltac_expr
| "info" ltac_expr
]

fun_var_list: [
| fun_var_list fun_var
| fun_var
]

fun_var: [
| ident
| "_"
]

rec_opt: [
| "rec"
| empty
]

let_clause_list: [
| let_clause_list "with" let_clause
| let_clause
]

let_clause: [
| ident ":=" ltac_expr
| "_" ":=" ltac_expr
| ident fun_var_list ":=" ltac_expr
]

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

multi_goal_tactics: [
| ltac_expr_opt "|" multi_goal_tactics
| ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
| ltac_expr
| empty
]

ltac_expr_opt: [
| ltac_expr
| empty
]

ltac_expr_opt_list_or: [
| ltac_expr_opt_list_or "|" ltac_expr_opt
| ltac_expr_opt
]

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

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

ltac_expr1: [
| ltac_match_term
| ltac_match_goal
| "first" "[" ltac_expr_list_or_opt "]"
| "solve" "[" ltac_expr_list_or_opt "]"
| "idtac" message_token_list_opt
| failkw int_or_var_opt message_token_list_opt
| simple_tactic
| tactic_arg
| qualid tactic_arg_compat_list_opt
| ltac_expr0
]

ltac_expr_list_or_opt: [
| ltac_expr_list_or
| empty
]

ltac_expr_list_or: [
| ltac_expr_list_or "|" ltac_expr
| ltac_expr
]

message_token_list_opt: [
| message_token_list_opt message_token
| empty
]

message_token: [
| ident
| string
| int
]

int_or_var_opt: [
| int_or_var
| empty
]

term1_extended_list_opt: [
| term1_extended_list_opt term1_extended
| empty
]

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

tactic_arg: [
| "eval" red_expr "in" term
| "context" ident "[" term "]"
| "type" "of" term
| "fresh" fresh_id_list_opt
| "type_term" term1_extended
| "numgoals"
]

fresh_id_list_opt: [
| fresh_id_list_opt fresh_id
| empty
]

fresh_id: [
| string
| qualid
]

tactic_arg_compat_list_opt: [
| tactic_arg_compat_list_opt tactic_arg_compat
| empty
]

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

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

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

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

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

selector: [
| range_selector_list_comma
| "[" ident "]"
]

range_selector_list_comma: [
| range_selector_list_comma "," range_selector
| range_selector
]

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

ltac_match_term: [
| match_key ltac_expr "with" or_opt match_rule_list_or "end"
]

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

match_rule_list_or: [
| match_rule_list_or "|" match_rule
| match_rule
]

match_rule: [
| match_pattern_alt "=>" ltac_expr
]

match_pattern_alt: [
| match_pattern
| "_"
]

match_pattern: [
| "context" ident_opt "[" term "]"
| term
]

ltac_match_goal: [
| match_key reverse_opt "goal" "with" or_opt match_context_rule_list_or "end"
]

reverse_opt: [
| "reverse"
| empty
]

match_context_rule_list_or: [
| match_context_rule_list_or "|" match_context_rule
| match_context_rule
]

match_context_rule: [
| match_hyp_list_comma_opt "|-" match_pattern "=>" ltac_expr
| "[" match_hyp_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr
| "_" "=>" ltac_expr
]

match_hyp_list_comma_opt: [
| match_hyp_list_comma
| empty
]

match_hyp_list_comma: [
| match_hyp_list_comma "," match_hyp
| match_hyp
]

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

match_pattern_opt: [
| "[" match_pattern "]" ":"
| empty
]

ident_list_opt: [
| ident_list_opt ident
| empty
]