Use counts for parser productions - coq/coq GitHub Wiki
Using https://github.com/coq/coq/pull/10652, I counted the number of times each Coq grammar production is used across the CI build:base, library:* and plugin:* jobs. Tactics are listed under "simple_tactic". Perhaps some of unused tactics can be deprecated.
372 ((gallina_ext : 765) : 764): LIST0 more_implicits_bloc
0 ((gallina_ext : 800) : 799): "Variable"
403 ((gallina_ext : 800) : 799): "Variables"
341 ((return_type : 381) : 380): "as" name
0 ((univ_decl : 317) : 317):
0 ((univ_decl : 317) : 317): "+"
0 ((univ_decl : 318) : 318): "}"
0 ((univ_decl : 318) : 318): bar_cbrace
0 (as_dirpath : 1102): "as" dirpath
8463 (binder_constr : 286): "(" LIST0 name SEP "," ")"
0 (binder_constr : 286): "()"
17856 (binder_tactic : 192):
713 (binder_tactic : 192): "rec"
186 (by_notation : 120): "%" IDENT
434 (case_item : 372): "as" name
465 (case_item : 373): "in" pattern200
837 (closed_binder : 127): "&"
651 (closed_binder : 127): "of"
31 (command : 101):
93 (command : 101): "discriminated"
0 (command : 354): "using" G_vernac.section_subset_expr
0 (command : 357): "with" Pltac.tactic
0 (command : 927):
0 (command : 927): "Verbose"
0 (command : 928): IDENT
0 (command : 928): ne_string
16244 (constructor_type : 511): of_type_with_opt_coercion lconstr
10199 (constructor_type : 513):
155 (corec_definition : 428): ":=" lconstr
31 (gallina : 199): "with" ident_decl binders ":" lconstr
0 (gallina : 232): ":" lconstr
124 (gallina_ext : 710): strategy_level "[" LIST1 smart_global "]"
0 (gallina_ext : 713): "Structure"
465 (gallina_ext : 713): OPT univ_decl def_body
0 (gallina_ext : 720): "Structure"
1271 (gallina_ext : 743): ":=" "{" record_declaration "}"
16802 (gallina_ext : 744):
1488 (gallina_ext : 744): ":=" lconstr
0 (gallina_ext : 752): "|" natural
372 (gallina_ext : 765): "," LIST1 [ LIST0 more_implicits_block ] SEP ","
713 (gallina_ext : 767): ":" LIST1 arguments_modifier SEP ","
0 (gallina_ext : 797): "All" "Variables"
0 (gallina_ext : 798): "No" "Variables"
403 (gallina_ext : 800): [ "Variable" | "Variables" ] LIST1 identref
8711 (inductive_definition : 393): ":" lconstr
0 (let_clause : 247): "_"
0 (mode : 135): "+"
0 (mode : 136): "!"
0 (mode : 137): "-"
372 (one_decl_notation : 377): ":" IDENT
27714 (opt_hintbases : 54): IDENT
12462 (option_table : 1099): IDENT
0 (printable : 1062):
0 (printable : 1062): "Sorted"
0 (range_selector_or_nth : 329): "," LIST1 range_selector SEP ","
62 (range_selector_or_nth : 332): "," LIST1 range_selector SEP ","
18662 (rec_definition : 421): ":=" lconstr
248 (record_field : 467): "|" natural
403 (return_type : 381): OPT [ "as" name ] case_type
155 (rewriter : 505): "?"
10447 (rewriter : 505): LEFTQMARK
0 (rewriter : 507): "?"
31 (rewriter : 507): LEFTQMARK
279 (simple_intropattern : 327): "%" operconstr0
0 (simple_tactic : 634): "," pattern_occ as_name
0 (simple_tactic : 653): "simple" "inversion"
0 (simple_tactic : 654): "inversion"
0 (simple_tactic : 655): "inversion_clear"
0 (simple_tactic : 657): "with" constr
0 (ssr_idcomma : 2631): "_"
0 (ssr_idcomma : 2631): IDENT
0 (ssrbinder : 1362): "&"
0 (ssrbinder : 1362): "of"
93 (ssrrule_ne : 2310): "/" ssrterm
2015 (ssrrule_ne : 2311): ssrterm
372 (ssrrule_ne : 2312): ssrsimpl_ne
6231 (syntax : 1201):
3658 (syntax : 1201): "(" LIST1 syntax_modifier SEP "," ")"
6820 (syntax : 1202): ":" IDENT
12834 (syntax : 1210):
6665 (syntax : 1210): "(" LIST1 syntax_modifier SEP "," ")"
11129 (syntax : 1211): ":" IDENT
0 (syntax : 1217):
0 (syntax : 1217): "(" LIST1 syntax_modifier SEP "," ")"
0 (syntax : 1223):
6634 (syntax : 1223): "(" LIST1 syntax_modifier SEP "," ")"
5084 (syntax_modifier : 1253): STRING
0 (syntax_modifier : 1254): STRING
310 (syntax_modifier : 1258): IDENT
1860 (tactic_expr1 : 155):
2356 (tactic_expr1 : 155): int_or_var
868 (type_cstr : 537): ":" lconstr
0 (typeclass_constraint : 527):
0 (typeclass_constraint : 527): "!"
2480 (typeclass_constraint : 529):
0 (typeclass_constraint : 529): "!"
0 (univ_constraint : 311): "<"
0 (univ_constraint : 311): "<="
0 (univ_constraint : 311): "="
0 (univ_decl : 315):
0 (univ_decl : 315): "+"
0 (univ_decl : 317): "|" LIST0 univ_constraint SEP "," [ "+" | ] "}"
0 (univ_decl : 318): [ "}" | bar_cbrace ]
0 Constr.closed_binder: "(" Prim.name ":" Constr.lconstr "|" Constr.lconstr ")"
64108 Constr.ident: Prim.ident
207297 Prim.ident: IDENT ssr_null_entry
0 Prim.name: "_"
7905 appl_arg: lpar_id_coloneq lconstr ")"
3888051 appl_arg: operconstr9
21979 argument_spec: OPT "!" name OPT scope
0 argument_spec_block: "&"
465 argument_spec_block: "(" LIST1 argument_spec ")" OPT scope
155 argument_spec_block: "/"
2449 argument_spec_block: "[" LIST1 argument_spec "]" OPT scope
3627 argument_spec_block: "{" LIST1 argument_spec "}" OPT scope
11532 argument_spec_block: argument_spec
0 arguments_modifier: "assert"
0 arguments_modifier: "clear" "bidirectionality" "hint"
155 arguments_modifier: "clear" "implicits"
0 arguments_modifier: "clear" "implicits" "and" "scopes"
31 arguments_modifier: "clear" "scopes"
0 arguments_modifier: "clear" "scopes" "and" "implicits"
93 arguments_modifier: "default" "implicits"
0 arguments_modifier: "extra" "scopes"
31 arguments_modifier: "rename"
372 arguments_modifier: "simpl" "never"
62 arguments_modifier: "simpl" "nomatch"
0 as_dirpath: OPT [ "as" dirpath ]
44144 as_ipat:
3658 as_ipat: "as" simple_intropattern
186 as_name:
1953 as_name: "as" ident
205127 as_or_and_ipat:
88691 as_or_and_ipat: "as" or_and_intropattern_loc
6324 assum_coe: "(" simple_assum_coe ")"
2294 assum_list: LIST1 assum_coe
43555 assum_list: simple_assum_coe
4898 assumption_token: "Axiom"
0 assumption_token: "Conjecture"
4681 assumption_token: "Hypothesis"
11377 assumption_token: "Parameter"
21483 assumption_token: "Variable"
0 assumptions_token: "Axioms"
0 assumptions_token: "Conjectures"
62 assumptions_token: "Hypotheses"
186 assumptions_token: "Parameters"
3162 assumptions_token: "Variables"
93 ast_closure_lterm: term_annotation lconstr
2015 ast_closure_term: term_annotation constr
0 at_level: "at" level
0 atomic_constr: "?" "[" ident "]"
0 atomic_constr: "?" "[" pattern_ident "]"
207266 atomic_constr: "_"
582645 atomic_constr: NUMERAL
8922885 atomic_constr: global instance
62124 atomic_constr: pattern_ident evar_instance
80383 atomic_constr: sort
5301 atomic_constr: string
5673 attribute: ident attribute_value
5518 attribute_list: LIST0 attribute SEP ","
2604 attribute_value:
2759 attribute_value: "(" attribute_list ")"
310 attribute_value: "=" string
0 auto_using':
0 auto_using': "using" constr_comma_sequence'
285541 auto_using:
7936 auto_using: "using" LIST1 uconstr SEP ","
279 bar_cbrace: test_nospace_pipe_closedcurly "|" "}"
150536 basequalid: ident
18228 basequalid: ident fields
31 bigint: NUMERAL
217713 binder: closed_binder
229648 binder: name
319517 binder_constr: "forall" open_binders "," operconstr200
74059 binder_constr: "fun" open_binders "=>" operconstr200
248 binder_constr: "if" operconstr200 "is" ssr_dthen ssr_else
0 binder_constr: "if" operconstr200 "isn't" ssr_dthen ssr_else
12462 binder_constr: "if" operconstr200 return_type "then" operconstr200 "else" operconstr200
930 binder_constr: "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
0 binder_constr: "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
0 binder_constr: "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
434 binder_constr: "let" ":" ssr_mpat ":=" lconstr "in" lconstr
0 binder_constr: "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr
31 binder_constr: "let" ":" ssr_mpat "in" pattern ":=" lconstr ssr_rtype "in" lconstr
8463 binder_constr: "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200
7037 binder_constr: "let" name binders type_cstr ":=" operconstr200 "in" operconstr200
93 binder_constr: "let" single_fix "in" operconstr200
1364 binder_constr: fix_constr
4185 binder_tactic: "fun" LIST1 input_fun "=>" tactic_expr5
0 binder_tactic: "info" tactic_expr5
18569 binder_tactic: "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5
800978 binders: LIST0 binder
1178 binders: Pcoq.Constr.binders
16802 binders_fixannot:
36239 binders_fixannot: binder binders_fixannot
3596 binders_fixannot: fixannot
1271 binders_fixannot: impl_name_head impl_ident_tail binders_fixannot
124434 bindings: LIST1 constr
17608 bindings: test_lpar_idnum_coloneq LIST1 simple_binding
14787 bindings_with_parameters: check_for_coloneq "(" ident LIST0 simple_binder ":=" lconstr ")"
47771 branches: OPT "|" LIST0 eqn SEP "|"
39990 by_arg_tac:
9114 by_arg_tac: "by" tactic3
310 by_notation: ne_string OPT [ "%" IDENT ]
561100 by_tactic:
34379 by_tactic: "by" tactic_expr3
51801 case_item: operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
1705 case_type: "return" operconstr100
0 casted_constr: constr
5146 check_module_type: "<:" module_type_inl
22816 check_module_types: LIST0 check_module_type
186 class_rawexpr: "Funclass"
186 class_rawexpr: "Sortclass"
1860 class_rawexpr: smart_global
1364 clause_dft_all:
93 clause_dft_all: "in" in_clause
0 clause_dft_concl:
146413 clause_dft_concl: "in" in_clause
873115 clause_dft_concl: occs
31 closed_binder: "'" pattern0
183861 closed_binder: "(" name ":" lconstr ")"
0 closed_binder: "(" name ":" lconstr ":=" lconstr ")"
124 closed_binder: "(" name ":=" lconstr ")"
48701 closed_binder: "(" name LIST1 name ":" lconstr ")"
7409 closed_binder: "`(" LIST1 typeclass_constraint SEP "," ")"
3751 closed_binder: "`{" LIST1 typeclass_constraint SEP "," "}"
6293 closed_binder: "{" name ":" lconstr "}"
7378 closed_binder: "{" name "}"
2418 closed_binder: "{" name LIST1 name ":" lconstr "}"
2821 closed_binder: "{" name LIST1 name "}"
1488 closed_binder: [ "of" | "&" ] operconstr99
0 cofixdecl: "(" ident LIST0 simple_binder ":" lconstr ")"
0 command: "Abort"
0 command: "Abort" "All"
0 command: "Abort" identref
124 command: "Add" "Field" ident ":" constr OPT field_mods
0 command: "Add" "LoadPath" ne_string as_dirpath
0 command: "Add" "ML" "Path" ne_string
0 command: "Add" "Morphism" constr ":" ident
2263 command: "Add" "Morphism" constr "with" "signature" lconstr "as" ident
899 command: "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" ident
0 command: "Add" "Parametric" "Relation" binders ":" constr constr "as" ident
0 command: "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
0 command: "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
279 command: "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
0 command: "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
0 command: "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident
0 command: "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
0 command: "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident
0 command: "Add" "Parametric" "Setoid" binders ":" constr constr constr "as" ident
0 command: "Add" "Rec" "LoadPath" ne_string as_dirpath
0 command: "Add" "Rec" "ML" "Path" ne_string
0 command: "Add" "Relation" constr constr "as" ident
0 command: "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" ident
0 command: "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
124 command: "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
31 command: "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
0 command: "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" ident
0 command: "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
0 command: "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident
341 command: "Add" "Ring" ident ":" constr OPT ring_mods
0 command: "Add" "Setoid" constr constr constr "as" ident
279 command: "Add" IDENT IDENT LIST1 option_ref_value
0 command: "Add" IDENT LIST1 option_ref_value
0 command: "AddPath" ne_string "as" as_dirpath
0 command: "AddRecPath" ne_string "as" as_dirpath
0 command: "Admit" "Obligations"
0 command: "Admit" "Obligations" "of" ident
0 command: "Admitted"
0 command: "Back"
0 command: "Back" natural
0 command: "Cd"
0 command: "Cd" ne_string
0 command: "Comments" LIST0 comment
124 command: "Create" "HintDb" IDENT; [ "discriminated" | ]
0 command: "Debug" "Off"
0 command: "Debug" "On"
0 command: "Declare" "Custom" "Entry" IDENT
372 command: "Declare" "Equivalent" "Keys" constr constr
1054 command: "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info
155 command: "Declare" "Left" "Step" constr
899 command: "Declare" "ML" "Module" LIST1 ne_string
0 command: "Declare" "Morphism" constr ":" ident
0 command: "Declare" "Reduction" IDENT; ":=" red_expr
155 command: "Declare" "Right" "Step" constr
1674 command: "Declare" "Scope" IDENT
12648 command: "Defined"
0 command: "Defined" identref
0 command: "DelPath" ne_string
0 command: "Derive" "Dependent" "Inversion" ident "with" constr "Sort" sort_family
0 command: "Derive" "Dependent" "Inversion_clear" ident "with" constr "Sort" sort_family
0 command: "Derive" "Inversion" ident "with" constr
0 command: "Derive" "Inversion" ident "with" constr "Sort" sort_family
0 command: "Derive" "Inversion_clear" ident "with" constr
0 command: "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family
0 command: "Derive" ident "SuchThat" constr "As" ident
0 command: "Existential" natural constr_body
4402 command: "Extract" "Constant" global LIST0 string "=>" mlname
1457 command: "Extract" "Inductive" global "=>" mlname "[" LIST0 mlname "]" OPT string
1829 command: "Extract" "Inlined" "Constant" global "=>" mlname
0 command: "Extraction" "Blacklist" LIST1 ident
0 command: "Extraction" "Implicit" global "[" LIST0 int_or_id "]"
62 command: "Extraction" "Inline" LIST1 global
0 command: "Extraction" "Language" language
0 command: "Extraction" "Library" ident
0 command: "Extraction" "NoInline" LIST1 global
0 command: "Extraction" "TestCompile" LIST1 global
0 command: "Extraction" global
0 command: "Extraction" string LIST1 global
0 command: "Focus"
0 command: "Focus" natural
372 command: "Function" LIST1 function_rec_definition_loc SEP "with"
0 command: "Functional" "Case" fun_scheme_arg
620 command: "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with"
0 command: "Generate" "graph" "for" reference
0 command: "Goal" lconstr
0 command: "Grab" "Existential" "Variables"
0 command: "Guarded"
0 command: "Hint" "Cut" "[" hints_path "]" opthints
0 command: "Hint" "Rewrite" orient LIST1 constr
1426 command: "Hint" "Rewrite" orient LIST1 constr ":" LIST0 preident
0 command: "Hint" "Rewrite" orient LIST1 constr "using" tactic
0 command: "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST0 preident
217 command: "Hint" "View" ssrviewposspc LIST1 ssrhintref
27683 command: "Hint" hint opt_hintbases
0 command: "Inspect" natural
0 command: "Load" [ "Verbose" | ] [ ne_string | IDENT ]
0 command: "Locate" "Ltac" reference
0 command: "Locate" locatable
21824 command: "Ltac" LIST1 ltac_tacdef_body SEP "with"
0 command: "Next" "Obligation" "of" ident withtac
1488 command: "Next" "Obligation" withtac
651 command: "Numeral" "Notation" reference reference reference ":" ident numnotoption
465 command: "Obligation" "Tactic" ":=" tactic
0 command: "Obligation" integer ":" lglob withtac
0 command: "Obligation" integer "of" ident ":" lglob withtac
0 command: "Obligation" integer "of" ident withtac
0 command: "Obligation" integer withtac
0 command: "Obligations"
0 command: "Obligations" "of" ident
0 command: "Optimize" "Heap"
0 command: "Optimize" "Proof"
217 command: "Prenex" "Implicits" LIST1 global
0 command: "Preterm"
0 command: "Preterm" "of" ident
0 command: "Print" "Equivalent" "Keys"
0 command: "Print" "Extraction" "Blacklist"
0 command: "Print" "Extraction" "Inline"
0 command: "Print" "Fields"
0 command: "Print" "Firstorder" "Solver"
0 command: "Print" "Hint" "View" ssrviewpos
0 command: "Print" "Ltac" "Signatures"
0 command: "Print" "Ltac" reference
0 command: "Print" "Module" "Type" global
0 command: "Print" "Module" global
0 command: "Print" "Namespace" dirpath
0 command: "Print" "Rewrite" "HintDb" preident
0 command: "Print" "Rings"
0 command: "Print" "Table" option_table
0 command: "Print" printable
0 command: "Print" smart_global OPT univ_name_list
347541 command: "Proof"
0 command: "Proof" "Mode" string
310 command: "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ]
992 command: "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
4464 command: "Proof" lconstr
0 command: "Pwd"
344503 command: "Qed"
0 command: "Recursive" "Extraction" "Library" ident
0 command: "Recursive" "Extraction" LIST1 global
31 command: "Remove" "Hints" LIST1 global opt_hintbases
0 command: "Remove" "LoadPath" ne_string
0 command: "Remove" IDENT IDENT LIST1 option_ref_value
0 command: "Remove" IDENT LIST1 option_ref_value
0 command: "Reset" "Extraction" "Blacklist"
0 command: "Reset" "Extraction" "Inline"
0 command: "Reset" "Initial"
0 command: "Reset" "Ltac" "Profile"
0 command: "Reset" identref
0 command: "Restart"
0 command: "Restore" "State" IDENT
0 command: "Restore" "State" ne_string
0 command: "Save" identref
0 command: "Search" ssr_search_arg ssr_modlocs
0 command: "Separate" "Extraction" LIST1 global
0 command: "Set" "Firstorder" "Solver" tactic
3875 command: "Set" option_table option_setting
0 command: "Show"
0 command: "Show" "Conjectures"
0 command: "Show" "Existentials"
0 command: "Show" "Extraction"
0 command: "Show" "Intro"
0 command: "Show" "Intros"
0 command: "Show" "Ltac" "Profile"
0 command: "Show" "Ltac" "Profile" "CutOff" int
0 command: "Show" "Ltac" "Profile" string
0 command: "Show" "Match" reference
0 command: "Show" "Obligation" "Tactic"
0 command: "Show" "Proof"
0 command: "Show" "Universes"
0 command: "Show" ident
0 command: "Show" natural
0 command: "Solve" "All" "Obligations"
0 command: "Solve" "All" "Obligations" "with" tactic
0 command: "Solve" "Obligation" integer "of" ident "with" tactic
0 command: "Solve" "Obligation" integer "with" tactic
0 command: "Solve" "Obligations"
0 command: "Solve" "Obligations" "of" ident "with" tactic
155 command: "Solve" "Obligations" "with" tactic
93 command: "String" "Notation" reference reference reference ":" ident
4402 command: "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
0 command: "Test" option_table
0 command: "Test" option_table "for" LIST1 option_ref_value
0 command: "Type" lconstr
403 command: "Typeclasses" "Opaque" LIST0 reference
0 command: "Typeclasses" "Transparent" LIST0 reference
0 command: "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int
0 command: "Undo"
0 command: "Undo" "To" natural
0 command: "Undo" natural
0 command: "Unfocus"
0 command: "Unfocused"
2263 command: "Unset" option_table
0 command: "Unshelve"
0 command: "Write" "State" IDENT
0 command: "Write" "State" ne_string
0 comment: STRING
0 comment: constr
0 comment: natural
0 comparison: "<"
0 comparison: "<="
0 comparison: "="
0 comparison: ">"
0 comparison: ">="
186 concl_occ:
6138 concl_occ: "*" occs
2387 constr: "@" global instance
2327666 constr: operconstr8
0 constr_as_binder_kind: "as" "ident"
0 constr_as_binder_kind: "as" "pattern"
0 constr_as_binder_kind: "as" "strict" "pattern"
0 constr_body: ":" lconstr ":=" lconstr
0 constr_body: ":=" lconstr
0 constr_comma_sequence': constr
0 constr_comma_sequence': constr "," constr_comma_sequence'
341 constr_eval: "context" identref "[" Constr.lconstr "]"
1550 constr_eval: "eval" red_expr "in" Constr.constr
0 constr_eval: "type" "of" Constr.constr
0 constr_may_eval: Constr.constr
0 constr_may_eval: constr_eval
3286 constr_pattern: constr
1675085 constr_with_bindings: constr with_bindings
0 constr_with_bindings_arg: ">" constr_with_bindings
1663119 constr_with_bindings_arg: constr_with_bindings
22165 constructor: identref constructor_type
124 constructor_list_or_record_decl:
1023 constructor_list_or_record_decl: "{" record_fields "}"
4433 constructor_list_or_record_decl: "|" LIST1 constructor SEP "|"
1891 constructor_list_or_record_decl: identref "{" record_fields "}"
3906 constructor_list_or_record_decl: identref constructor_type
372 constructor_list_or_record_decl: identref constructor_type "|" LIST0 constructor SEP "|"
26443 constructor_type: binders [ of_type_with_opt_coercion lconstr | ]
6386 conversion: constr
31 conversion: constr "at" occs_nums "with" constr
9331 conversion: constr "with" constr
155 corec_definition: ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation
0 cpattern: "Qed" constr
4061 cpattern: ssrtermkind constr
0 cumulativity_token: "Cumulative"
0 cumulativity_token: "NonCumulative"
0 debug:
0 debug: "debug"
43183 decl_notation:
372 decl_notation: "where" LIST1 one_decl_notation SEP decl_sep
0 decl_sep: "and"
3845302 decorated_vernac: LIST0 quoted_attributes vernac
6975 def_body: binders ":" lconstr
33728 def_body: binders ":" lconstr ":=" reduce lconstr
61752 def_body: binders ":=" reduce lconstr
96131 def_token: "Definition"
1240 def_token: "Example"
0 def_token: "SubClass"
154535 delta_flag:
62 delta_flag: "-" "[" LIST1 smart_global "]"
1085 delta_flag: "[" LIST1 smart_global "]"
264616 destruction_arg: constr_with_bindings_arg
10881 destruction_arg: natural
62 destruction_arg: test_lpar_id_rpar constr_with_bindings
0 dirpath: ident LIST0 field
0 eauto_search_strategy:
0 eauto_search_strategy: "(bfs)"
0 eauto_search_strategy: "(dfs)"
2635 eliminator: "using" constr_with_bindings
179304 eqn: LIST1 mult_pattern SEP "|" "=>" lconstr
269483 eqn_ipat:
0 eqn_ipat: "_eqn"
0 eqn_ipat: "_eqn" ":" naming_intropattern
2108 eqn_ipat: "eqn" ":" naming_intropattern
6944 equality_intropattern: "->"
3937 equality_intropattern: "<-"
3410 equality_intropattern: "[=" intropatterns "]"
62124 evar_instance:
0 evar_instance: "@{" LIST1 inst SEP ";" "}"
23405 export_token:
15035 export_token: "Export"
39339 export_token: "Import"
1271 ext_module_expr: "<+" module_expr_inl
7719 ext_module_type: "<+" module_type_inl
4216 failkw: "fail"
0 failkw: "gfail"
414160 field: FIELD
93 field_mod: "completeness" constr
248 field_mod: ring_mod
93 field_mods: "(" LIST1 field_mod SEP "," ")"
397451 fields: field
16709 fields: field fields
2356 finite_token: "Class"
217 finite_token: "CoInductive"
6789 finite_token: "Inductive"
1984 finite_token: "Record"
372 finite_token: "Structure"
465 finite_token: "Variant"
7595 firstorder_using:
217 firstorder_using: "using" reference
31 firstorder_using: "using" reference "," LIST1 reference SEP ","
0 firstorder_using: "using" reference reference LIST0 reference
1364 fix_constr: single_fix
0 fix_constr: single_fix "with" LIST1 fix_decl SEP "with" "for" identref
1457 fix_decl: identref binders_fixannot type_cstr ":=" operconstr200
0 fix_kw: "cofix"
1457 fix_kw: "fix"
0 fixannot:
31 fixannot: "{" "measure" constr OPT identref OPT constr "}"
3565 fixannot: "{" "struct" identref "}"
0 fixannot: "{" "struct" name "}"
0 fixannot: "{" "wf" constr identref "}"
0 fixdecl: "(" ident LIST0 simple_binder fixannot ":" lconstr ")"
4371 fresh_id: STRING
527 fresh_id: qualid
930 fullyqualid: ident
465 fullyqualid: ident fields
2759 fun_ind_using:
0 fun_ind_using: "using" constr_with_bindings
620 fun_scheme_arg: ident ":=" "Induction" "for" reference "Sort" sort_family
372 function_rec_definition_loc: Vernac.rec_definition
44485 functor_app_annot:
0 functor_app_annot: "[" "inline" "at" "level" natural "]"
0 functor_app_annot: "[" "no" "inline" "]"
155 gallina: "CoFixpoint" LIST1 corec_definition SEP "with"
0 gallina: "Combined" "Scheme" identref "from" LIST1 identref SEP ","
0 gallina: "Constraint" LIST1 univ_constraint SEP ","
18445 gallina: "Fixpoint" LIST1 rec_definition SEP "with"
0 gallina: "Let" "CoFixpoint" LIST1 corec_definition SEP "with"
0 gallina: "Let" "Fixpoint" LIST1 rec_definition SEP "with"
4123 gallina: "Let" identref def_body
775 gallina: "Primitive" identref OPT [ ":" lconstr ] ":=" register_token
372 gallina: "Register" "Inline" global
8494 gallina: "Register" global "as" qualid
496 gallina: "Scheme" LIST1 scheme SEP "with"
0 gallina: "Universe" LIST1 identref
0 gallina: "Universes" LIST1 identref
12183 gallina: OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
42439 gallina: assumption_token inline assum_list
3410 gallina: assumptions_token inline assum_list
97371 gallina: def_token ident_decl def_body
335172 gallina: thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
7533 gallina_ext: "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
0 gallina_ext: "Canonical" OPT "Structure" by_notation
589 gallina_ext: "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ]
0 gallina_ext: "Chapter" identref
0 gallina_ext: "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr
496 gallina_ext: "Coercion" global ":" class_rawexpr ">->" class_rawexpr
496 gallina_ext: "Coercion" global OPT univ_decl def_body
0 gallina_ext: "Collection" identref ":=" section_subset_expr
1054 gallina_ext: "Context" LIST1 binder
310 gallina_ext: "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl
27280 gallina_ext: "End" identref
0 gallina_ext: "Existing" "Class" global
310 gallina_ext: "Existing" "Instance" global hint_info
0 gallina_ext: "Existing" "Instances" LIST1 global OPT [ "|" natural ]
0 gallina_ext: "Export" "Set" option_table option_setting
0 gallina_ext: "Export" "Unset" option_table
837 gallina_ext: "Export" LIST1 global
62 gallina_ext: "From" global "Require" export_token LIST1 global
403 gallina_ext: "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
93 gallina_ext: "Identity" "Coercion" identref ":" class_rawexpr ">->" class_rawexpr
868 gallina_ext: "Implicit" "Type" reserv_list
992 gallina_ext: "Implicit" "Types" reserv_list
0 gallina_ext: "Import" "Prenex" "Implicits"
3007 gallina_ext: "Import" LIST1 global
0 gallina_ext: "Include" "Type" module_type_inl LIST0 ext_module_type
4061 gallina_ext: "Include" module_type_inl LIST0 ext_module_expr
19561 gallina_ext: "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
9331 gallina_ext: "Module" "Type" identref LIST0 module_binder check_module_types is_module_type
13609 gallina_ext: "Module" export_token identref LIST0 module_binder of_module_type is_module_expr
341 gallina_ext: "Opaque" LIST1 smart_global
47802 gallina_ext: "Require" export_token LIST1 global
14415 gallina_ext: "Section" identref
124 gallina_ext: "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
93 gallina_ext: "Transparent" LIST1 smart_global
0 glob: constr
0 glob_constr_with_bindings: constr_with_bindings
9118867 global: Prim.reference
0 hat: "^" "~" ident
0 hat: "^" "~" natural
0 hat: "^" ident
0 hat: "^~" ident
0 hat: "^~" natural
31 hint: "Constants" "Opaque"
0 hint: "Constants" "Transparent"
1488 hint: "Constructors" LIST1 global
3534 hint: "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
3689 hint: "Immediate" LIST1 reference_or_constr
0 hint: "Mode" global mode
0 hint: "Opaque" LIST1 global
0 hint: "Resolve" "->" LIST1 global OPT natural
0 hint: "Resolve" "<-" LIST1 global OPT natural
16740 hint: "Resolve" LIST1 reference_or_constr hint_info
124 hint: "Transparent" LIST1 global
2015 hint: "Unfold" LIST1 global
62 hint: "Variables" "Opaque"
0 hint: "Variables" "Transparent"
35464 hint_info:
2201 hint_info: "|" OPT natural OPT constr_pattern
211885 hintbases:
7812 hintbases: "with" "*"
73873 hintbases: "with" LIST1 preident
0 hints_path: "(" hints_path ")"
0 hints_path: "emp"
0 hints_path: "eps"
0 hints_path: hints_path "*"
0 hints_path: hints_path "|" hints_path
0 hints_path: hints_path hints_path
0 hints_path: hints_path_atom
0 hints_path_atom: "_"
0 hints_path_atom: LIST1 global
0 hloc:
0 hloc: "in" "(" "Type" "of" ident ")"
0 hloc: "in" "(" "Value" "of" ident ")"
0 hloc: "in" "(" "type" "of" ident ")"
0 hloc: "in" "(" "value" "of" ident ")"
0 hloc: "in" "|-" "*"
0 hloc: "in" ident
0 hypident: "(" "type" "of" Prim.identref ")"
0 hypident: "(" "type" "of" id_or_meta ")"
0 hypident: "(" "value" "of" Prim.identref ")"
0 hypident: "(" "value" "of" id_or_meta ")"
124000 hypident: id_or_meta
124000 hypident_occ: hypident occs
146444 id_or_meta: identref
13545946 ident: IDENT
542686 ident_decl: identref OPT univ_decl
9672 ident_no_do: test_ident_no_do IDENT
933100 identref: ident
310 impl_ident_tail: ":" lconstr "}"
682 impl_ident_tail: "}"
93 impl_ident_tail: LIST1 name ":" lconstr "}"
186 impl_ident_tail: LIST1 name "}"
1271 impl_name_head: impl_ident_head
186 in_clause: "*" "|-" concl_occ
22878 in_clause: "*" occs
119598 in_clause: LIST0 hypident_occ SEP ","
6138 in_clause: LIST0 hypident_occ SEP "," "|-" concl_occ
0 in_clause: in_clause'
595324 in_hyp_as:
22444 in_hyp_as: "in" id_or_meta as_ipat
23684 in_hyp_list:
0 in_hyp_list: "in" LIST1 id_or_meta
0 in_or_out_modules:
0 in_or_out_modules: ne_in_or_out_modules
270134 induction_clause: destruction_arg as_or_and_ipat eqn_ipat opt_clause
262570 induction_clause_list: LIST1 induction_clause SEP "," OPT eliminator opt_clause
12214 inductive_definition: opt_coercion ident_decl binders OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation
44702 inline:
930 inline: "Inline"
217 inline: "Inline" "(" natural ")"
1333 input_fun: "_"
39649 input_fun: ident
0 inst: ident ":=" lconstr
8960054 instance:
0 instance: "@{" LIST0 universe_level "}"
465 instance_name:
19096 instance_name: ident_decl binders
0 int_or_id: integer
0 int_or_id: preident
155 int_or_var: identref
20367 int_or_var: integer
155 integer: "-" NUMERAL
21979 integer: NUMERAL
1054 intropattern: "*"
93 intropattern: "**"
733057 intropattern: simple_intropattern
182528 intropatterns: LIST0 intropattern
7905 is_module_expr:
5704 is_module_expr: ":=" module_expr_inl LIST0 ext_module_expr
4960 is_module_type:
4371 is_module_type: ":=" module_type_inl LIST0 ext_module_type
0 language: "Haskell"
0 language: "JSON"
0 language: "OCaml"
0 language: "Ocaml"
0 language: "Scheme"
0 lconstr: l_constr
1352747 lconstr: operconstr200
63023 lconstr_pattern: lconstr
0 lcpattern: "Qed" lconstr
0 lcpattern: ssrtermkind lconstr
0 let_clause: "_" ":=" tactic_expr
17515 let_clause: identref ":=" tactic_expr
1984 let_clause: identref LIST1 input_fun ":=" tactic_expr
2542 level: "level" natural
372 level: "next" "level"
0 lglob: lconstr
0 locatable: "File" ne_string
0 locatable: "Library" global
0 locatable: "Module" global
0 locatable: "Term" smart_global
0 locatable: smart_global
19499 lstring: string
0 ltac_def_kind: "::="
21855 ltac_def_kind: ":="
0 ltac_info: "Info" natural
0 ltac_production_item: ident
6634 ltac_production_item: ident "(" ident OPT ltac_production_sep ")"
11718 ltac_production_item: string
0 ltac_production_sep: "," string
0 ltac_selector: toplevel_selector
0 ltac_tacdef_body: tacdef_body
372 ltac_tactic_level: "(" "at" "level" natural ")"
2134846 ltac_use_default: "."
5332 ltac_use_default: "..."
47771 match_constr: "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
7254 match_context_list: "|" LIST1 match_context_rule SEP "|"
2883 match_context_list: LIST1 match_context_rule SEP "|"
5921 match_context_rule: "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr
3038 match_context_rule: "_" "=>" tactic_expr
23343 match_context_rule: LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr
16802 match_hyps: name ":" match_pattern
0 match_hyps: name ":=" "[" match_pattern "]" ":" match_pattern
217 match_hyps: name ":=" match_pattern
527 match_key: "lazymatch"
17329 match_key: "match"
0 match_key: "multimatch"
6045 match_list: "|" LIST1 match_rule SEP "|"
1674 match_list: LIST1 match_rule SEP "|"
11563 match_pattern: "context" OPT Constr.ident "[" Constr.lconstr_pattern "]"
51460 match_pattern: Constr.lconstr_pattern
4340 match_rule: "_" "=>" tactic_expr
16740 match_rule: match_pattern "=>" tactic_expr
2666 message_token: STRING
620 message_token: identref
0 message_token: integer
1178 mlname: preident
25141 mlname: string
0 mode: LIST1 [ "+" | "!" | "-" ]
0 modloc: "-" global
0 modloc: global
15996 module_binder: "(" export_token LIST1 identref ":" module_type_inl ")"
5828 module_expr: module_expr module_expr_atom
8246 module_expr: module_expr_atom
1271 module_expr_atom: "(" module_expr ")"
29202 module_expr_atom: qualid
155 module_expr_inl: "!" module_expr
6820 module_expr_inl: module_expr functor_app_annot
0 module_type: "(" module_type ")"
1395 module_type: module_type "with" with_declaration
16399 module_type: module_type module_expr_atom
37727 module_type: qualid
62 module_type_inl: "!" module_type
37665 module_type_inl: module_type functor_app_annot
341 more_implicits_block: "[" LIST1 name "]"
0 more_implicits_block: "{" LIST1 name "}"
713 more_implicits_block: name
180947 mult_pattern: LIST1 pattern200 SEP ","
20367 name: "_"
1226360 name: ident
8215 naming_intropattern: "?"
754292 naming_intropattern: ident
310 naming_intropattern: pattern_ident
0 nat_or_var: identref
19344 nat_or_var: natural
86986 natural: NUMERAL
0 natural: _natural
0 ne_in_or_out_modules: "inside" LIST1 global
0 ne_in_or_out_modules: "outside" LIST1 global
198090 ne_intropatterns: LIST1 intropattern
16895 ne_lstring: ne_string
18104 ne_string: STRING
0 noedit_mode: query_command
620 numnotoption:
31 numnotoption: "(" "abstract" "after" bigint ")"
0 numnotoption: "(" "warning" "after" bigint ")"
1273759 occs:
18507 occs: "at" occs_nums
155 occs_nums: "-" nat_or_var LIST0 int_or_var
18414 occs_nums: LIST1 nat_or_var
62 occurrences: LIST1 integer
62 occurrences: var
124 of_module_type: ":" module_type_inl
13485 of_module_type: check_module_types
76818 of_type_with_opt_coercion: ":"
0 of_type_with_opt_coercion: ":" ">"
0 of_type_with_opt_coercion: ":" ">" ">"
1488 of_type_with_opt_coercion: ":>"
0 of_type_with_opt_coercion: ":>" ">"
0 of_type_with_opt_coercion: ":>>"
372 one_decl_notation: ne_lstring ":=" constr OPT [ ":" IDENT ]
7409 only_parsing:
0 only_parsing: "(" "compat" STRING ")"
27683 only_parsing: "(" "only" "parsing" ")"
46562 open_binders: closed_binder binders
0 open_binders: name ".." name
135780 open_binders: name LIST0 name ":" lconstr
230237 open_binders: name LIST0 name binders
0 open_constr: constr
1806618 operconstr0: "(" operconstr200 ")"
0 operconstr0: "`(" operconstr200 ")"
0 operconstr0: "`{" operconstr200 "}"
124 operconstr0: "ltac" ":" "(" Pltac.tactic_expr ")"
310 operconstr0: "{" binder_constr "}"
279 operconstr0: "{|" record_declaration bar_cbrace
9860604 operconstr0: atomic_constr
47771 operconstr0: match_constr
2573 operconstr100: operconstr ":" SELF
31 operconstr100: operconstr ":" binder_constr
186 operconstr100: operconstr ":>"
0 operconstr100: operconstr "<:" SELF
0 operconstr100: operconstr "<:" binder_constr
0 operconstr100: operconstr "<<:" SELF
0 operconstr100: operconstr "<<:" binder_constr
34782 operconstr10: "@" global instance LIST0 NEXT
62 operconstr10: "@" pattern_identref LIST1 identref
2341151 operconstr10: operconstr LIST1 appl_arg
79639 operconstr1: operconstr "%" IDENT
0 operconstr1: operconstr ".(" "@" global LIST0 ( operconstr9 ) ")"
93 operconstr1: operconstr ".(" global LIST0 appl_arg ")"
446152 operconstr200: binder_constr
434 operconstr9: ".." operconstr0 ".."
532146 opt_clause:
31 opt_clause: "at" occs_nums
527 opt_clause: "in" in_clause
12214 opt_coercion:
0 opt_coercion: ">"
465 opt_constructors_or_fields:
11749 opt_constructors_or_fields: ":=" constructor_list_or_record_decl
0 opt_hintbases:
27714 opt_hintbases: ":" LIST1 IDENT
0 opthints:
0 opthints: ":" LIST1 preident
93 option_ref_value: STRING
248 option_ref_value: global
3596 option_setting:
124 option_setting: STRING
155 option_setting: integer
6138 option_table: LIST1 IDENT
5394 or_and_intropattern: "(" simple_intropattern "&" LIST1 simple_intropattern SEP "&" ")"
31 or_and_intropattern: "(" simple_intropattern ")"
51305 or_and_intropattern: "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
0 or_and_intropattern: "()"
99448 or_and_intropattern: "[" LIST1 intropatterns SEP "|" "]"
62 or_and_intropattern_loc: identref
88629 or_and_intropattern_loc: or_and_intropattern
514321 orient:
3007 orient: "->"
153853 orient: "<-"
671181 oriented_rewriter: orient rewriter
2821 pattern0: "(" pattern200 ")"
0 pattern0: "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
31961 pattern0: "_"
0 pattern0: "{|" record_patterns bar_cbrace
88970 pattern0: NUMERAL
255192 pattern0: Prim.reference
434 pattern0: string
0 pattern100: pattern ":" binder_constr
0 pattern100: pattern ":" operconstr100
589 pattern10: "@" Prim.reference LIST0 NEXT
155 pattern10: pattern "as" name
71920 pattern10: pattern LIST1 NEXT
155 pattern1: pattern "%" IDENT
62496 pattern_ident: LEFTQMARK ident
62 pattern_identref: pattern_ident
9982 pattern_occ: constr occs
0 positive_search_mark:
0 positive_search_mark: "-"
79887 preident: IDENT
0 printable: "All"
0 printable: "All" "Dependencies" smart_global
0 printable: "Assumptions" smart_global
0 printable: "Canonical" "Projections"
0 printable: "Classes"
0 printable: "Coercion" "Paths" class_rawexpr class_rawexpr
0 printable: "Coercions"
0 printable: "Custom" "Grammar" IDENT
0 printable: "Debug" "GC"
0 printable: "Grammar" IDENT
0 printable: "Graph"
0 printable: "Hint"
0 printable: "Hint" "*"
0 printable: "Hint" smart_global
0 printable: "HintDb" IDENT
0 printable: "Implicit" smart_global
0 printable: "Instances" smart_global
0 printable: "Libraries"
0 printable: "LoadPath" OPT dirpath
0 printable: "ML" "Modules"
0 printable: "ML" "Path"
0 printable: "Modules"
0 printable: "Opaque" "Dependencies" smart_global
0 printable: "Options"
0 printable: "Registered"
0 printable: "Scope" IDENT
0 printable: "Scopes"
0 printable: "Section" global
0 printable: "Strategies"
0 printable: "Strategy" smart_global
0 printable: "Tables"
0 printable: "Term" smart_global OPT univ_name_list
0 printable: "Transparent" "Dependencies" smart_global
0 printable: "TypeClasses"
0 printable: "Typing" "Flags"
0 printable: "Visibility" OPT IDENT
0 printable: [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
0 printunivs_subgraph: "Subgraph" "(" LIST0 reference ")"
3334050 private_token:
0 private_token: "Private"
168764 qualid: basequalid
23281 quantified_hypothesis: ident
6262 quantified_hypothesis: natural
0 query_command: "About" smart_global OPT univ_name_list "."
0 query_command: "Check" lconstr "."
0 query_command: "Compute" lconstr "."
0 query_command: "Eval" red_expr "in" lconstr "."
0 query_command: "Search" searchabout_query searchabout_queries "."
0 query_command: "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
0 query_command: "SearchAbout" searchabout_query searchabout_queries "."
0 query_command: "SearchHead" constr_pattern in_or_out_modules "."
0 query_command: "SearchPattern" constr_pattern in_or_out_modules "."
0 query_command: "SearchRewrite" constr_pattern in_or_out_modules "."
2759 quoted_attributes: "#[" attribute_list "]"
62 range_selector: natural
0 range_selector: natural "-" natural
0 range_selector_or_nth: natural "-" natural OPT [ "," LIST1 range_selector SEP "," ]
5146 range_selector_or_nth: natural OPT [ "," LIST1 range_selector SEP "," ]
18941 rec_definition: ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation
31 record_binder: name
12214 record_binder: name record_binder_body
31 record_binder_body: binders ":=" lconstr
12090 record_binder_body: binders of_type_with_opt_coercion lconstr
93 record_binder_body: binders of_type_with_opt_coercion lconstr ":=" lconstr
1550 record_declaration: record_fields
12245 record_field: LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation
6975 record_field_declaration: global binders ":=" lconstr
93 record_fields:
2821 record_fields: record_field
0 record_fields: record_field ";"
9424 record_fields: record_field ";" record_fields
1147 record_fields: record_field_declaration
5828 record_fields: record_field_declaration ";" record_fields
0 record_pattern: global ":=" pattern200
0 record_patterns:
0 record_patterns: record_pattern
0 record_patterns: record_pattern ";"
0 record_patterns: record_pattern ";" record_patterns
0 red_expr: "cbn" strategy_flag
403 red_expr: "cbv" strategy_flag
961 red_expr: "compute" delta_flag
0 red_expr: "fold" LIST1 constr
62 red_expr: "hnf"
341 red_expr: "lazy" strategy_flag
0 red_expr: "native_compute" OPT ref_or_pattern_occ
0 red_expr: "pattern" LIST1 pattern_occ SEP ","
248 red_expr: "red"
93 red_expr: "simpl" delta_flag OPT ref_or_pattern_occ
155 red_expr: "unfold" LIST1 unfold_occ SEP ","
124 red_expr: "vm_compute" OPT ref_or_pattern_occ
31 red_expr: IDENT
806 red_flags: "beta"
0 red_flags: "cofix"
434 red_flags: "delta" delta_flag
0 red_flags: "fix"
93 red_flags: "iota"
0 red_flags: "match"
217 red_flags: "zeta"
94612 reduce:
868 reduce: "Eval" red_expr "in"
775 ref_or_pattern_occ: constr occs
5487 ref_or_pattern_occ: smart_global occs
9921147 reference: ident
378758 reference: ident fields
0 reference_or_constr: constr
42904 reference_or_constr: global
31 register_prim_token: "#int63_add"
31 register_prim_token: "#int63_addc"
31 register_prim_token: "#int63_addcarryc"
31 register_prim_token: "#int63_addmuldiv"
31 register_prim_token: "#int63_compare"
31 register_prim_token: "#int63_div"
31 register_prim_token: "#int63_div21"
31 register_prim_token: "#int63_diveucl"
31 register_prim_token: "#int63_eq"
31 register_prim_token: "#int63_head0"
31 register_prim_token: "#int63_land"
31 register_prim_token: "#int63_le"
31 register_prim_token: "#int63_lor"
31 register_prim_token: "#int63_lsl"
31 register_prim_token: "#int63_lsr"
31 register_prim_token: "#int63_lt"
31 register_prim_token: "#int63_lxor"
31 register_prim_token: "#int63_mod"
31 register_prim_token: "#int63_mul"
31 register_prim_token: "#int63_mulc"
31 register_prim_token: "#int63_sub"
31 register_prim_token: "#int63_subc"
31 register_prim_token: "#int63_subcarryc"
31 register_prim_token: "#int63_tail0"
744 register_token: register_prim_token
31 register_token: register_type_token
31 register_type_token: "#int63_type"
1054 rename: ident "into" ident
62 reserv_list: LIST1 reserv_tuple
1798 reserv_list: simple_reserv
124 reserv_tuple: "(" simple_reserv ")"
20925 return_type: OPT [ OPT [ "as" name ] case_type ]
17918 rewriter: "!" constr_with_bindings_arg
10602 rewriter: [ "?" | LEFTQMARK ] constr_with_bindings_arg
629393 rewriter: constr_with_bindings_arg
1085 rewriter: natural "!" constr_with_bindings_arg
31 rewriter: natural [ "?" | LEFTQMARK ] constr_with_bindings_arg
12152 rewriter: natural constr_with_bindings_arg
0 rewstrategy: "(" rewstrategy ")"
0 rewstrategy: "<-" constr
0 rewstrategy: "any" rewstrategy
0 rewstrategy: "bottomup" rewstrategy
0 rewstrategy: "choice" rewstrategy rewstrategy
0 rewstrategy: "eval" red_expr
0 rewstrategy: "fail"
0 rewstrategy: "fold" constr
0 rewstrategy: "hints" preident
0 rewstrategy: "id"
0 rewstrategy: "innermost" rewstrategy
0 rewstrategy: "old_hints" preident
0 rewstrategy: "outermost" rewstrategy
0 rewstrategy: "progress" rewstrategy
0 rewstrategy: "refl"
0 rewstrategy: "repeat" rewstrategy
0 rewstrategy: "subterm" rewstrategy
0 rewstrategy: "subterms" rewstrategy
0 rewstrategy: "terms" LIST0 constr
0 rewstrategy: "topdown" rewstrategy
0 rewstrategy: "try" rewstrategy
0 rewstrategy: glob
0 rewstrategy: rewstrategy ";" rewstrategy
0 ring_mod: "abstract"
0 ring_mod: "closed" "[" LIST1 global "]"
279 ring_mod: "constants" "[" tactic "]"
186 ring_mod: "decidable" constr
31 ring_mod: "div" constr
62 ring_mod: "morphism" constr
31 ring_mod: "postprocess" "[" tactic "]"
0 ring_mod: "power" constr "[" LIST1 global "]"
124 ring_mod: "power_tac" constr "[" tactic "]"
62 ring_mod: "preprocess" "[" tactic "]"
0 ring_mod: "setoid" constr constr
31 ring_mod: "sign" constr
186 ring_mods: "(" LIST1 ring_mod SEP "," ")"
0 rpattern: "in" lconstr
0 rpattern: "in" lconstr "in" lconstr
155 rpattern: lconstr
0 rpattern: lconstr "as" lconstr "in" lconstr
0 rpattern: lconstr "in" lconstr
0 rpattern: lconstr "in" lconstr "in" lconstr
496 scheme: identref ":=" scheme_kind
0 scheme: scheme_kind
0 scheme_kind: "Case" "for" smart_global "Sort" sort_family
0 scheme_kind: "Elimination" "for" smart_global "Sort" sort_family
0 scheme_kind: "Equality" "for" smart_global
496 scheme_kind: "Induction" "for" smart_global "Sort" sort_family
0 scheme_kind: "Minimality" "for" smart_global "Sort" sort_family
0 scope: "%" IDENT
0 searchabout_queries:
0 searchabout_queries: ne_in_or_out_modules
0 searchabout_queries: searchabout_query searchabout_queries
0 searchabout_query: positive_search_mark constr_pattern
0 searchabout_query: positive_search_mark ne_string OPT scope
310 section_subset_expr: only_starredidentrefs LIST0 starredidentref
0 section_subset_expr: ssexpr
0 selector: "only" selector_body ":"
5146 selector_body: range_selector_or_nth
0 selector_body: test_bracket_ident "[" ident "]"
49879 simple_assum_coe: LIST1 ident_decl of_type_with_opt_coercion lconstr
248 simple_binder: "(" LIST1 name ":" lconstr ")"
465 simple_binder: name
16120 simple_binding: "(" ident ":=" lconstr ")"
5363 simple_binding: "(" natural ":=" lconstr ")"
860901 simple_intropattern: simple_intropattern_closed LIST0 [ "%" operconstr0 ]
18352 simple_intropattern_closed: "_"
14291 simple_intropattern_closed: equality_intropattern
760709 simple_intropattern_closed: naming_intropattern
67549 simple_intropattern_closed: or_and_intropattern
1922 simple_reserv: LIST1 identref ":" lconstr
0 simple_tactic: "abstract" ssrdgens
3224 simple_tactic: "absurd" constr
31 simple_tactic: "admit"
186 simple_tactic: "apply"
608313 simple_tactic: "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
2108 simple_tactic: "apply" ssrapplyarg
19468 simple_tactic: "assert" constr as_ipat by_tactic
32891 simple_tactic: "assert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
28551 simple_tactic: "assert" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
107105 simple_tactic: "assumption"
222549 simple_tactic: "auto" OPT int_or_var auto_using hintbases
0 simple_tactic: "autoapply" constr "using" preident
31 simple_tactic: "autoapply" constr "with" preident
0 simple_tactic: "autorewrite" "*" "with" LIST1 preident clause
0 simple_tactic: "autorewrite" "*" "with" LIST1 preident clause "using" tactic
1023 simple_tactic: "autorewrite" "with" LIST1 preident clause
31 simple_tactic: "autorewrite" "with" LIST1 preident clause "using" tactic
0 simple_tactic: "autounfold" hintbases clause_dft_concl
0 simple_tactic: "autounfold_one" hintbases
0 simple_tactic: "autounfold_one" hintbases "in" hyp
0 simple_tactic: "btauto"
9517 simple_tactic: "by" ssrhintarg
1488 simple_tactic: "case"
39401 simple_tactic: "case" induction_clause_list
4154 simple_tactic: "case" ssrcasearg ssrclauses
0 simple_tactic: "casetype" constr
3348 simple_tactic: "cbn" strategy_flag clause_dft_concl
806 simple_tactic: "cbv" strategy_flag clause_dft_concl
15748 simple_tactic: "change" conversion clause_dft_concl
0 simple_tactic: "change_no_check" conversion clause_dft_concl
992 simple_tactic: "clear" "-" LIST1 hyp
47926 simple_tactic: "clear" LIST0 hyp
0 simple_tactic: "clear" natural
2635 simple_tactic: "clearbody" LIST1 hyp
62 simple_tactic: "cofix" ident
0 simple_tactic: "cofix" ident "with" LIST1 cofixdecl
0 simple_tactic: "compare" constr constr
3317 simple_tactic: "compute" delta_flag clause_dft_concl
155 simple_tactic: "congr" ssrcongrarg
5673 simple_tactic: "congruence"
0 simple_tactic: "congruence" "with" LIST1 constr
0 simple_tactic: "congruence" integer
0 simple_tactic: "congruence" integer "with" LIST1 constr
0 simple_tactic: "constr_eq" constr constr
0 simple_tactic: "constr_eq_nounivs" constr constr
0 simple_tactic: "constr_eq_strict" constr constr
13051 simple_tactic: "constructor"
2201 simple_tactic: "constructor" int_or_var
186 simple_tactic: "constructor" int_or_var "with" bindings
4557 simple_tactic: "contradiction" OPT constr_with_bindings
0 simple_tactic: "convert_concl_no_check" constr
24335 simple_tactic: "cut" constr
62 simple_tactic: "cutrewrite" orient constr
0 simple_tactic: "cutrewrite" orient constr "in" hyp
0 simple_tactic: "cycle" int_or_var
0 simple_tactic: "debug" "auto" OPT int_or_var auto_using hintbases
0 simple_tactic: "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
0 simple_tactic: "debug" "trivial" auto_using hintbases
310 simple_tactic: "decide" "equality"
2759 simple_tactic: "decompose" "[" LIST1 constr "]" constr
62 simple_tactic: "decompose" "record" constr
0 simple_tactic: "decompose" "sum" constr
0 simple_tactic: "dependent" "generalize_eqs" hyp
0 simple_tactic: "dependent" "generalize_eqs_vars" hyp
62 simple_tactic: "dependent" "rewrite" orient constr
0 simple_tactic: "dependent" "rewrite" orient constr "in" hyp
0 simple_tactic: "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" constr ]
0 simple_tactic: "destauto"
0 simple_tactic: "destauto" "in" hyp
176762 simple_tactic: "destruct" induction_clause_list
0 simple_tactic: "dfs" "eauto" OPT int_or_var auto_using hintbases
19158 simple_tactic: "discriminate"
2077 simple_tactic: "discriminate" destruction_arg
31 simple_tactic: "double" "induction" quantified_hypothesis quantified_hypothesis
9455 simple_tactic: "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
0 simple_tactic: "eassert" constr as_ipat by_tactic
0 simple_tactic: "eassert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
0 simple_tactic: "eassert" test_lpar_id_coloneq "(" identref ":=" lconstr ")"
651 simple_tactic: "eassumption"
14415 simple_tactic: "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
0 simple_tactic: "ecase" induction_clause_list
93 simple_tactic: "econstructor"
0 simple_tactic: "econstructor" int_or_var
0 simple_tactic: "econstructor" int_or_var "with" bindings
217 simple_tactic: "edestruct" induction_clause_list
0 simple_tactic: "ediscriminate"
0 simple_tactic: "ediscriminate" destruction_arg
0 simple_tactic: "eelim" constr_with_bindings_arg OPT eliminator
0 simple_tactic: "eenough" constr as_ipat by_tactic
0 simple_tactic: "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
31 simple_tactic: "eexact" constr
124 simple_tactic: "eexists"
0 simple_tactic: "eexists" LIST1 bindings SEP ","
0 simple_tactic: "einduction" induction_clause_list
0 simple_tactic: "einjection"
0 simple_tactic: "einjection" "as" LIST0 simple_intropattern
0 simple_tactic: "einjection" destruction_arg
0 simple_tactic: "einjection" destruction_arg "as" LIST0 simple_intropattern
0 simple_tactic: "eintros"
0 simple_tactic: "eintros" ne_intropatterns
0 simple_tactic: "eleft"
0 simple_tactic: "eleft" "with" bindings
0 simple_tactic: "elim"
94209 simple_tactic: "elim" constr_with_bindings_arg OPT eliminator
31 simple_tactic: "elim" ssrarg ssrclauses
248 simple_tactic: "elimtype" constr
713 simple_tactic: "enough" constr as_ipat by_tactic
93 simple_tactic: "enough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic
0 simple_tactic: "epose" "proof" lconstr as_ipat
0 simple_tactic: "epose" bindings_with_parameters
0 simple_tactic: "epose" constr as_name
0 simple_tactic: "eremember" constr as_name eqn_ipat clause_dft_all
248 simple_tactic: "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
0 simple_tactic: "eright"
0 simple_tactic: "eright" "with" bindings
0 simple_tactic: "eset" bindings_with_parameters clause_dft_concl
0 simple_tactic: "eset" constr as_name clause_dft_concl
0 simple_tactic: "esimplify_eq"
0 simple_tactic: "esimplify_eq" destruction_arg
0 simple_tactic: "esplit"
0 simple_tactic: "esplit" "with" bindings
558 simple_tactic: "etransitivity"
0 simple_tactic: "evar" constr
155 simple_tactic: "evar" test_lpar_id_colon "(" ident ":" lconstr ")"
31 simple_tactic: "exact"
0 simple_tactic: "exact" "<:" lconstr
42129 simple_tactic: "exact" casted_constr
620 simple_tactic: "exact" ssrexactarg
0 simple_tactic: "exact_no_check" constr
0 simple_tactic: "exists"
48329 simple_tactic: "exists" LIST1 bindings SEP ","
0 simple_tactic: "f_equal"
341 simple_tactic: "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr
31 simple_tactic: "finish_timing" "(" string ")" OPT string
0 simple_tactic: "finish_timing" OPT string
0 simple_tactic: "firstorder" OPT tactic "with" LIST1 preident
7781 simple_tactic: "firstorder" OPT tactic firstorder_using
0 simple_tactic: "firstorder" OPT tactic firstorder_using "with" LIST1 preident
372 simple_tactic: "fix" ident natural
0 simple_tactic: "fix" ident natural "with" LIST1 fixdecl
4309 simple_tactic: "fold" LIST1 constr clause_dft_concl
2759 simple_tactic: "functional" "induction" LIST1 constr fun_ind_using with_names
0 simple_tactic: "functional" "inversion" quantified_hypothesis OPT reference
0 simple_tactic: "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint
310 simple_tactic: "generalize" "dependent" constr
37634 simple_tactic: "generalize" constr
5270 simple_tactic: "generalize" constr LIST1 constr
248 simple_tactic: "generalize" constr lookup_at_as_comma occs as_name LIST0 [ "," pattern_occ as_name ]
93 simple_tactic: "generalize_eqs" hyp
31 simple_tactic: "generalize_eqs_vars" hyp
0 simple_tactic: "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint
0 simple_tactic: "gintuition" OPT tactic
0 simple_tactic: "give_up"
0 simple_tactic: "guard" test
0 simple_tactic: "has_evar" constr
0 simple_tactic: "have" "suff" ssrhpats_nobs ssrhavefwd
0 simple_tactic: "have" "suffices" ssrhpats_nobs ssrhavefwd
62 simple_tactic: "have" ssrhavefwdwbinders
62 simple_tactic: "head_of_constr" ident constr
0 simple_tactic: "hget_evar" int_or_var
124 simple_tactic: "hnf" clause_dft_concl
0 simple_tactic: "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr
0 simple_tactic: "hresolve_core" "(" ident ":=" constr ")" "in" constr
46190 simple_tactic: "induction" induction_clause_list
0 simple_tactic: "info_auto" OPT int_or_var auto_using hintbases
0 simple_tactic: "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases
0 simple_tactic: "info_trivial" auto_using hintbases
62 simple_tactic: "injection"
0 simple_tactic: "injection" "as" LIST0 simple_intropattern
1550 simple_tactic: "injection" destruction_arg
1767 simple_tactic: "injection" destruction_arg "as" LIST0 simple_intropattern
0 simple_tactic: "instantiate"
0 simple_tactic: "instantiate" "(" ident ":=" lglob ")"
0 simple_tactic: "instantiate" "(" integer ":=" lglob ")" hloc
59241 simple_tactic: "intro"
0 simple_tactic: "intro" "after" hyp
0 simple_tactic: "intro" "at" "bottom"
0 simple_tactic: "intro" "at" "top"
0 simple_tactic: "intro" "before" hyp
45260 simple_tactic: "intro" ident
0 simple_tactic: "intro" ident "after" hyp
0 simple_tactic: "intro" ident "at" "bottom"
0 simple_tactic: "intro" ident "at" "top"
0 simple_tactic: "intro" ident "before" hyp
216876 simple_tactic: "intros"
682 simple_tactic: "intros" "until" quantified_hypothesis
198090 simple_tactic: "intros" ne_intropatterns
0 simple_tactic: "inversion" quantified_hypothesis "using" constr in_hyp_list
14105 simple_tactic: "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
9548 simple_tactic: "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list
0 simple_tactic: "is_cofix" constr
0 simple_tactic: "is_const" constr
0 simple_tactic: "is_constructor" constr
0 simple_tactic: "is_evar" constr
0 simple_tactic: "is_fix" constr
0 simple_tactic: "is_ground" constr
0 simple_tactic: "is_ind" constr
0 simple_tactic: "is_proj" constr
124 simple_tactic: "is_var" constr
1612 simple_tactic: "lapply" constr
155 simple_tactic: "lazy" strategy_flag clause_dft_concl
32302 simple_tactic: "left"
0 simple_tactic: "left" "with" bindings
31 simple_tactic: "lra_Q" tactic
31 simple_tactic: "lra_R" tactic
0 simple_tactic: "move"
62 simple_tactic: "move" hyp "after" hyp
0 simple_tactic: "move" hyp "at" "bottom"
0 simple_tactic: "move" hyp "at" "top"
62 simple_tactic: "move" hyp "before" hyp
2976 simple_tactic: "move" ssrmovearg ssrclauses
62 simple_tactic: "move" ssrmovearg ssrrpat
186 simple_tactic: "move" ssrrpat
0 simple_tactic: "myred"
0 simple_tactic: "native_cast_no_check" constr
0 simple_tactic: "native_compute" OPT ref_or_pattern_occ clause_dft_concl
0 simple_tactic: "new" "auto" OPT int_or_var auto_using hintbases
62 simple_tactic: "not_evar" constr
0 simple_tactic: "notypeclasses" "refine" uconstr
0 simple_tactic: "nsatz_compute" constr
0 simple_tactic: "omega"
62 simple_tactic: "omega" "with" "*"
0 simple_tactic: "omega" "with" LIST1 ident
0 simple_tactic: "optimize_heap"
9579 simple_tactic: "pattern" LIST1 pattern_occ SEP "," clause_dft_concl
5177 simple_tactic: "pose" "proof" lconstr as_ipat
2046 simple_tactic: "pose" bindings_with_parameters
403 simple_tactic: "pose" constr as_name
0 simple_tactic: "pose" ssrcofixfwd
0 simple_tactic: "pose" ssrfixfwd
0 simple_tactic: "pose" ssrfwdid ssrposefwd
0 simple_tactic: "progress_evars" tactic
0 simple_tactic: "prolog" "[" LIST0 uconstr "]" int_or_var
93 simple_tactic: "protect_fv" string
124 simple_tactic: "protect_fv" string "in" ident
62 simple_tactic: "psatz_Q" int_or_var tactic
0 simple_tactic: "psatz_Q" tactic
62 simple_tactic: "psatz_R" int_or_var tactic
0 simple_tactic: "psatz_R" tactic
31 simple_tactic: "psatz_Z" int_or_var tactic
0 simple_tactic: "psatz_Z" tactic
22506 simple_tactic: "red" clause_dft_concl
2883 simple_tactic: "refine" uconstr
61194 simple_tactic: "reflexivity"
1457 simple_tactic: "remember" constr as_name eqn_ipat clause_dft_all
930 simple_tactic: "rename" LIST1 rename SEP ","
0 simple_tactic: "replace" "->" uconstr clause
0 simple_tactic: "replace" "<-" uconstr clause
49104 simple_tactic: "replace" uconstr "with" constr clause by_arg_tac
0 simple_tactic: "replace" uconstr clause
0 simple_tactic: "reset" "ltac" "profile"
31 simple_tactic: "restart_timer" OPT string
11067 simple_tactic: "revert" LIST1 hyp
0 simple_tactic: "revgoals"
0 simple_tactic: "rewrite" "*" orient uconstr "at" occurrences "in" hyp by_arg_tac
0 simple_tactic: "rewrite" "*" orient uconstr "at" occurrences by_arg_tac
0 simple_tactic: "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac
0 simple_tactic: "rewrite" "*" orient uconstr "in" hyp by_arg_tac
0 simple_tactic: "rewrite" "*" orient uconstr by_arg_tac
542066 simple_tactic: "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic
1519 simple_tactic: "rewrite" ssrrwargs ssrclauses
62 simple_tactic: "rewrite_db" preident
0 simple_tactic: "rewrite_db" preident "in" hyp
0 simple_tactic: "rewrite_strat" rewstrategy
0 simple_tactic: "rewrite_strat" rewstrategy "in" hyp
23901 simple_tactic: "right"
434 simple_tactic: "right" "with" bindings
186 simple_tactic: "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr
0 simple_tactic: "rtauto"
12741 simple_tactic: "set" bindings_with_parameters clause_dft_concl
31 simple_tactic: "set" constr as_name clause_dft_concl
0 simple_tactic: "set" ssrfwdid ssrsetfwd ssrclauses
0 simple_tactic: "setoid_etransitivity"
0 simple_tactic: "setoid_reflexivity"
1674 simple_tactic: "setoid_rewrite" orient glob_constr_with_bindings
93 simple_tactic: "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences
0 simple_tactic: "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp
31 simple_tactic: "setoid_rewrite" orient glob_constr_with_bindings "in" hyp
31 simple_tactic: "setoid_rewrite" orient glob_constr_with_bindings "in" hyp "at" occurrences
0 simple_tactic: "setoid_symmetry"
0 simple_tactic: "setoid_symmetry" "in" hyp
0 simple_tactic: "setoid_transitivity" constr
0 simple_tactic: "shelve"
0 simple_tactic: "shelve_unifiable"
0 simple_tactic: "show" "ltac" "profile"
0 simple_tactic: "show" "ltac" "profile" "cutoff" int
0 simple_tactic: "show" "ltac" "profile" string
146971 simple_tactic: "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl
0 simple_tactic: "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
279 simple_tactic: "simple" "destruct" quantified_hypothesis
0 simple_tactic: "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as
4836 simple_tactic: "simple" "induction" quantified_hypothesis
0 simple_tactic: "simple" "injection"
31 simple_tactic: "simple" "injection" destruction_arg
31 simple_tactic: "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list
0 simple_tactic: "simple" "notypeclasses" "refine" uconstr
0 simple_tactic: "simple" "refine" uconstr
0 simple_tactic: "simple" "subst"
0 simple_tactic: "simplify_eq"
0 simple_tactic: "simplify_eq" destruction_arg
0 simple_tactic: "soft" "functional" "induction" LIST1 constr fun_ind_using with_names
0 simple_tactic: "solve_constraints"
62 simple_tactic: "sos_Q" tactic
62 simple_tactic: "sos_R" tactic
31 simple_tactic: "sos_Z" tactic
6851 simple_tactic: "specialize" constr_with_bindings
248 simple_tactic: "specialize" constr_with_bindings "as" simple_intropattern
31 simple_tactic: "specialize_eqs" hyp
75361 simple_tactic: "split"
3255 simple_tactic: "split" "with" bindings
0 simple_tactic: "ssrinstancesofruleL2R" ssrterm
0 simple_tactic: "ssrinstancesofruleR2L" ssrterm
0 simple_tactic: "ssrinstancesoftpat" cpattern
0 simple_tactic: "start" "ltac" "profiling"
0 simple_tactic: "stepl" constr
124 simple_tactic: "stepl" constr "by" tactic
0 simple_tactic: "stepr" constr
124 simple_tactic: "stepr" constr "by" tactic
0 simple_tactic: "stop" "ltac" "profiling"
10540 simple_tactic: "subst"
4805 simple_tactic: "subst" LIST1 var
93 simple_tactic: "substitute" orient glob_constr_with_bindings
0 simple_tactic: "suff" "have" ssrhpats_nobs ssrhavefwd
0 simple_tactic: "suff" ssrsufffwd
0 simple_tactic: "suffices" "have" ssrhpats_nobs ssrhavefwd
0 simple_tactic: "suffices" ssrsufffwd
0 simple_tactic: "swap" int_or_var int_or_var
19003 simple_tactic: "symmetry"
1767 simple_tactic: "symmetry" "in" in_clause
7781 simple_tactic: "transitivity" constr
0 simple_tactic: "transparent_abstract" tactic3
0 simple_tactic: "transparent_abstract" tactic3 "using" ident
56327 simple_tactic: "trivial" auto_using hintbases
0 simple_tactic: "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
155 simple_tactic: "typeclasses" "eauto" OPT int_or_var
31 simple_tactic: "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
0 simple_tactic: "under" ssrrwarg
0 simple_tactic: "under" ssrrwarg "do" ssrhint3arg
0 simple_tactic: "under" ssrrwarg ssrintros_ne
0 simple_tactic: "under" ssrrwarg ssrintros_ne "do" ssrhint3arg
206894 simple_tactic: "unfold" LIST1 unfold_occ SEP "," clause_dft_concl
31 simple_tactic: "unify" constr constr
31 simple_tactic: "unify" constr constr "with" preident
93 simple_tactic: "unlock" ssrunlockargs ssrclauses
248 simple_tactic: "unshelve" tactic1
186 simple_tactic: "vm_cast_no_check" constr
496 simple_tactic: "vm_compute" OPT ref_or_pattern_occ clause_dft_concl
0 simple_tactic: "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint
0 simple_tactic: "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint
0 simple_tactic: "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint
0 simple_tactic: "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint
0 simple_tactic: "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint
0 simple_tactic: "wlog" ssrhpats_nobs ssrwlogfwd ssrhint
31 simple_tactic: "xlia" tactic
31 simple_tactic: "xnlia" tactic
31 simple_tactic: "xnqa" tactic
31 simple_tactic: "xnra" tactic
1457 single_fix: fix_kw fix_decl
310 smart_global: by_notation
267189 smart_global: reference
40517 sort: "Prop"
186 sort: "SProp"
3379 sort: "Set"
36301 sort: "Type"
0 sort: "Type" "@{" "_" "}"
0 sort: "Type" "@{" universe "}"
1054 sort_family: "Prop"
0 sort_family: "SProp"
31 sort_family: "Set"
31 sort_family: "Type"
0 ssexpr0: "(" only_starredidentrefs LIST0 starredidentref ")"
0 ssexpr0: "(" only_starredidentrefs LIST0 starredidentref ")" "*"
0 ssexpr0: "(" ssexpr ")"
0 ssexpr0: "(" ssexpr ")" "*"
0 ssexpr0: starredidentref
0 ssexpr35: "-" ssexpr
0 ssexpr50: ssexpr "+" ssexpr
0 ssexpr50: ssexpr "-" ssexpr
155 ssr_dpat: ssr_mpat
93 ssr_dpat: ssr_mpat "in" pattern ssr_rtype
0 ssr_dpat: ssr_mpat ssr_rtype
248 ssr_dthen: ssr_dpat "then" lconstr
248 ssr_else: ssr_elsepat lconstr
248 ssr_elsepat: "else"
0 ssr_first: "[" LIST0 tactic_expr SEP "|" "]"
0 ssr_first: ssr_first ssrintros_ne
0 ssr_first_else: ssr_first
0 ssr_first_else: ssr_first ssrorelse
0 ssr_idcomma:
0 ssr_idcomma: test_idcomma [ IDENT | "_" ] ","
0 ssr_modlocs:
0 ssr_modlocs: "in" LIST1 modloc
713 ssr_mpat: pattern
124 ssr_rtype: "return" operconstr100
0 ssr_search_arg:
0 ssr_search_arg: "-" ssr_search_item ssr_search_arg
0 ssr_search_arg: ssr_search_item ssr_search_arg
0 ssr_search_item: constr_pattern
0 ssr_search_item: string
0 ssr_search_item: string "%" preident
0 ssragen: "{" LIST1 ssrhyp "}" ssrterm
2170 ssragen: ssrterm
2170 ssragens:
0 ssragens: "{" LIST1 ssrhyp "}"
0 ssragens: "{" LIST1 ssrhyp "}" ssrterm ssragens
1085 ssragens: ssrterm ssragens
1550 ssrapplyarg: ":" ssragen ssragens ssrintros
0 ssrapplyarg: ssrbwdview ":" ssragen ssragens ssrintros
527 ssrapplyarg: ssrbwdview ssrclear ssrintros
0 ssrapplyarg: ssrclear_ne ssrintros
31 ssrapplyarg: ssrintros_ne
0 ssrarg: ssrclear_ne ssrintros
3813 ssrarg: ssreqid ssrdgens ssrintros
527 ssrarg: ssrfwdview ssrclear ssrintros
31 ssrarg: ssrfwdview ssreqid ssrdgens ssrintros
2852 ssrarg: ssrintros_ne
0 ssrbinder: "(" ssrbvar ")"
0 ssrbinder: "(" ssrbvar ":" lconstr ")"
0 ssrbinder: "(" ssrbvar ":" lconstr ":=" lconstr ")"
0 ssrbinder: "(" ssrbvar ":=" lconstr ")"
0 ssrbinder: "(" ssrbvar LIST1 ssrbvar ":" lconstr ")"
0 ssrbinder: [ "of" | "&" ] operconstr99
0 ssrbinder: ssrbvar
0 ssrbvar: "_"
0 ssrbvar: ident
527 ssrbwdview: test_not_ssrslashnum "/" Pcoq.Constr.constr
186 ssrbwdview: test_not_ssrslashnum "/" Pcoq.Constr.constr ssrbwdview
4154 ssrcasearg: ssrarg
0 ssrclausehyps: ssrwgen
0 ssrclausehyps: ssrwgen "," ssrclausehyps
0 ssrclausehyps: ssrwgen ssrclausehyps
9641 ssrclauses:
0 ssrclauses: "in" "*"
0 ssrclauses: "in" "*" "|-"
0 ssrclauses: "in" "|-" "*"
0 ssrclauses: "in" ssrclausehyps
0 ssrclauses: "in" ssrclausehyps "*"
0 ssrclauses: "in" ssrclausehyps "|-"
0 ssrclauses: "in" ssrclausehyps "|-" "*"
1054 ssrclear:
0 ssrclear: ssrclear_ne
0 ssrclear_ne: "{" LIST1 ssrhyp "}"
0 ssrcofixfwd: "cofix" ssrbvar LIST0 ssrbinder ssrfwd
31 ssrcongrarg: constr
0 ssrcongrarg: constr ssrdgens
124 ssrcongrarg: natural constr
0 ssrcongrarg: natural constr ssrdgens
0 ssrcpat: test_nohidden "[" hat "]"
930 ssrcpat: test_nohidden "[" ssriorpat "]"
0 ssrcpat: test_nohidden "[=" ssriorpat "]"
3844 ssrdgens: ":" ssrgen ssrdgens_tl
3844 ssrdgens_tl:
93 ssrdgens_tl: "/" ssrdgens_tl
0 ssrdgens_tl: "{" LIST1 ssrhyp "}"
0 ssrdgens_tl: "{" LIST1 ssrhyp "}" cpattern ssrdgens_tl
0 ssrdgens_tl: "{" ssrocc "}" cpattern ssrdgens_tl
217 ssrdgens_tl: cpattern ssrdgens_tl
0 ssrdocc: "{" LIST0 ssrhyp "}"
124 ssrdocc: "{" ssrocc "}"
62 ssrdotac: ssrortacarg
775 ssrdotac: tactic_expr3
3720 ssreqid: test_ssreqid
124 ssreqid: test_ssreqid ssreqpat
0 ssreqpat: "+"
0 ssreqpat: "->"
0 ssreqpat: "<-"
0 ssreqpat: "?"
0 ssreqpat: "_"
124 ssreqpat: Prim.ident
0 ssreqpat: ssrdocc "->"
0 ssreqpat: ssrdocc "<-"
620 ssrexactarg: ":" ssragen ssragens
0 ssrexactarg: ssrbwdview ssrclear
0 ssrexactarg: ssrclear_ne
0 ssrfixfwd: "fix" ssrbvar LIST0 ssrbinder ssrstruct ssrfwd
0 ssrfwd: ":" ast_closure_lterm ":=" ast_closure_lterm
0 ssrfwd: ":=" ast_closure_lterm
0 ssrfwdid: test_ssrfwdid Prim.ident
1922 ssrfwdview: test_not_ssrslashnum "/" ast_closure_term
93 ssrfwdview: test_not_ssrslashnum "/" ast_closure_term ssrfwdview
3844 ssrgen: cpattern
0 ssrgen: ssrdocc cpattern
0 ssrhavefwd: ":" ast_closure_lterm ":="
31 ssrhavefwd: ":" ast_closure_lterm ":=" ast_closure_lterm
31 ssrhavefwd: ":" ast_closure_lterm ssrhint
0 ssrhavefwd: ":=" ast_closure_lterm
62 ssrhavefwdwbinders: ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd
0 ssrhint3arg: "[" "]"
0 ssrhint3arg: "[" ssrortacs "]"
0 ssrhint3arg: ssrtac3arg
31 ssrhint:
0 ssrhint: "by" ssrhintarg
868 ssrhintarg: "[" "]"
31 ssrhintarg: "[" ssrortacs "]"
8618 ssrhintarg: ssrtacarg
0 ssrhintref: constr
868 ssrhintref: constr "|" natural
0 ssrhoi_hyp: ident
0 ssrhoi_id: ident
62 ssrhpats: ssripats
31 ssrhpats_nobs: ssripats
93 ssrhpats_wtransp: ssripats
0 ssrhpats_wtransp: ssripats "@" ssripats
0 ssrhyp: ident
5084 ssrintros:
1364 ssrintros: ssrintros_ne
5270 ssrintros_ne: "=>" ssripats_ne
930 ssriorpat: ssripats
465 ssriorpat: ssripats "|" ssriorpat
0 ssriorpat: ssripats "|-" ">" ssriorpat
0 ssriorpat: ssripats "|-" ssriorpat
0 ssriorpat: ssripats "|->" ssriorpat
0 ssriorpat: ssripats "||" ssriorpat
0 ssriorpat: ssripats "|||" ssriorpat
0 ssriorpat: ssripats "||||" ssriorpat
279 ssripat: "*"
0 ssripat: "+"
0 ssripat: "++"
93 ssripat: "-"
0 ssripat: "-/" "/"
0 ssripat: "-/" "/="
0 ssripat: "-/" "="
0 ssripat: "-/" integer "/"
0 ssripat: "-/" integer "/" integer "="
0 ssripat: "-/" integer "/="
0 ssripat: "-//"
0 ssripat: "-//" "="
0 ssripat: "-//="
0 ssripat: "-/="
837 ssripat: "->"
124 ssripat: "<-"
0 ssripat: ">"
1023 ssripat: "?"
0 ssripat: "[" ":" LIST0 ident "]"
0 ssripat: "[:" LIST0 ident "]"
372 ssripat: "_"
9672 ssripat: ident_no_do
930 ssripat: ssrcpat
0 ssripat: ssrdocc
0 ssripat: ssrdocc "->"
124 ssripat: ssrdocc "<-"
1364 ssripat: ssrfwdview
1147 ssripat: ssrsimpl_ne
6851 ssripats:
10695 ssripats: ssripat ssripats
5270 ssripats_ne: ssripat ssripats
1054 ssrmmod: "!"
186 ssrmmod: "?"
248 ssrmmod: LEFTQMARK
3038 ssrmovearg: ssrarg
372 ssrmult:
217 ssrmult: ssrmult_ne
124 ssrmult_ne: natural ssrmmod
527 ssrmult_ne: ssrmmod
0 ssrocc: "+" LIST0 natural
0 ssrocc: "-" LIST0 natural
279 ssrocc: natural LIST0 natural
0 ssrorelse: "||" tactic_expr2
62 ssrortacarg: "[" ssrortacs "]"
0 ssrortacs: "|"
0 ssrortacs: "|" ssrortacs
93 ssrortacs: ssrtacarg
0 ssrortacs: ssrtacarg "|"
217 ssrortacs: ssrtacarg "|" ssrortacs
0 ssrparentacarg: "(" tactic_expr ")"
0 ssrpattern_ne_squarep: "[" rpattern "]"
899 ssrpattern_squarep:
155 ssrpattern_squarep: "[" rpattern "]"
0 ssrpatternarg: rpattern
0 ssrposefwd: LIST0 ssrbinder ssrfwd
124 ssrrpat: "->"
124 ssrrpat: "<-"
0 ssrrule:
0 ssrrule: ssrrule_ne
0 ssrrule_ne: ssrsimpl_ne
2480 ssrrule_ne: test_not_ssrslashnum [ "/" ssrterm | ssrterm | ssrsimpl_ne ]
589 ssrrwarg: "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne
0 ssrrwarg: "-/" ssrterm
0 ssrrwarg: "{" "}" ssrpattern_squarep ssrrule_ne
0 ssrrwarg: "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne
0 ssrrwarg: "{" LIST1 ssrhyp "}" ssrrule
31 ssrrwarg: "{" ssrocc "}" ssrpattern_squarep ssrrule_ne
434 ssrrwarg: ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne
0 ssrrwarg: ssrpattern_ne_squarep ssrrule_ne
1426 ssrrwarg: ssrrule_ne
1519 ssrrwargs: test_ssr_rw_syntax LIST1 ssrrwarg
899 ssrrwocc:
0 ssrrwocc: "{" LIST0 ssrhyp "}"
124 ssrrwocc: "{" ssrocc "}"
0 ssrseqarg: ssrseqidx ssrortacarg OPT ssrorelse
0 ssrseqarg: ssrseqidx ssrswap
0 ssrseqarg: ssrswap
434 ssrseqarg: tactic_expr3
0 ssrseqidx: Prim.natural
0 ssrseqidx: test_ssrseqvar Prim.ident
0 ssrsetfwd: ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern
0 ssrsetfwd: ":" ast_closure_lterm ":=" lcpattern
0 ssrsetfwd: ":=" "{" ssrocc "}" cpattern
0 ssrsetfwd: ":=" lcpattern
31 ssrsimpl_ne: "//="
465 ssrsimpl_ne: "/="
1023 ssrsimpl_ne: test_ssrslashnum00 "//"
0 ssrsimpl_ne: test_ssrslashnum01 "//" natural "="
0 ssrsimpl_ne: test_ssrslashnum10 "/" natural "/"
0 ssrsimpl_ne: test_ssrslashnum10 "/" natural "/" "="
0 ssrsimpl_ne: test_ssrslashnum10 "/" natural "/="
0 ssrsimpl_ne: test_ssrslashnum10 "/" natural "="
0 ssrsimpl_ne: test_ssrslashnum11 "/" natural "/" natural "="
0 ssrstruct:
0 ssrstruct: "{" "struct" ident "}"
0 ssrsufffwd: ssrhpats LIST0 ssrbinder ":" ast_closure_lterm ssrhint
0 ssrswap: "first"
0 ssrswap: "last"
0 ssrtac3arg: tactic_expr3
8928 ssrtacarg: tactic_expr5
0 ssrtclarg: ssrtacarg
5363 ssrterm: ssrtermkind Pcoq.Constr.constr
0 ssrunlockarg: "{" ssrocc "}" ssrterm
0 ssrunlockarg: ssrterm
124 ssrunlockargs: LIST0 ssrunlockarg
0 ssrviewpos:
93 ssrviewpos: "for" "apply" "/"
0 ssrviewpos: "for" "apply" "/" "/"
31 ssrviewpos: "for" "apply" "//"
93 ssrviewpos: "for" "move" "/"
0 ssrviewposspc: ssrviewpos
0 ssrwgen: "(" "@" ssrhoi_id ":=" lcpattern ")"
0 ssrwgen: "(" ssrhoi_id ")"
0 ssrwgen: "(" ssrhoi_id ":=" lcpattern ")"
0 ssrwgen: "(@" ssrhoi_id ":=" lcpattern ")"
0 ssrwgen: "@" ssrhoi_hyp
0 ssrwgen: ssrclear_ne
0 ssrwgen: ssrhoi_hyp
0 ssrwlogfwd: ":" LIST0 ssrwgen "/" ast_closure_lterm
0 starredidentref: "Type"
0 starredidentref: "Type" "*"
496 starredidentref: identref
0 starredidentref: identref "*"
1147 strategy_flag: LIST1 red_flags
3906 strategy_flag: delta_flag
93 strategy_level: "expand"
0 strategy_level: "opaque"
0 strategy_level: "transparent"
31 strategy_level: integer
79050 string: STRING
7254 subprf: "{"
7440 subprf: "}"
122388 subprf: BULLET
930 syntax: "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
682 syntax: "Close" "Scope" IDENT
1240 syntax: "Delimit" "Scope" IDENT; "with" IDENT
0 syntax: "Format" "Notation" STRING STRING STRING
9889 syntax: "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ]
35092 syntax: "Notation" identref LIST0 ident ":=" constr only_parsing
19499 syntax: "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ]
8463 syntax: "Open" "Scope" IDENT
0 syntax: "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
6634 syntax: "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ]
0 syntax: "Undelimit" "Scope" IDENT
0 syntax_extension_type: "bigint"
248 syntax_extension_type: "binder"
0 syntax_extension_type: "closed" "binder"
0 syntax_extension_type: "constr"
0 syntax_extension_type: "constr" OPT at_level OPT constr_as_binder_kind
0 syntax_extension_type: "custom" IDENT OPT at_level OPT constr_as_binder_kind
0 syntax_extension_type: "global"
2046 syntax_extension_type: "ident"
0 syntax_extension_type: "pattern"
31 syntax_extension_type: "pattern" "at" "level" natural
248 syntax_extension_type: "strict" "pattern"
0 syntax_extension_type: "strict" "pattern" "at" "level" natural
15748 syntax_modifier: "at" "level" natural
0 syntax_modifier: "compat" STRING
5084 syntax_modifier: "format" STRING OPT STRING
0 syntax_modifier: "in" "custom" IDENT
0 syntax_modifier: "in" "custom" IDENT; "at" "level" natural
1426 syntax_modifier: "left" "associativity"
4774 syntax_modifier: "no" "associativity"
1240 syntax_modifier: "only" "parsing"
248 syntax_modifier: "only" "printing"
2015 syntax_modifier: "right" "associativity"
0 syntax_modifier: IDENT constr_as_binder_kind
2573 syntax_modifier: IDENT syntax_extension_type
155 syntax_modifier: IDENT; "," LIST1 IDENT SEP "," "at" level
2759 syntax_modifier: IDENT; "at" level
0 syntax_modifier: IDENT; "at" level constr_as_binder_kind
10137 tacdef_body: Constr.global LIST1 input_fun ltac_def_kind tactic_expr
11718 tacdef_body: Constr.global ltac_def_kind tactic_expr
2297565 tactic: tactic_expr
5642 tactic_arg: "fresh" LIST0 fresh_id
0 tactic_arg: "numgoals"
0 tactic_arg: "type_term" uconstr
4371 tactic_arg: constr_eval
589 tactic_arg_compat: "()"
123349 tactic_arg_compat: Constr.constr
4123 tactic_arg_compat: tactic_arg
0 tactic_atom: "()"
93 tactic_atom: integer
0 tactic_atom: reference
32550 tactic_expr0: "(" tactic_expr ")"
31 tactic_expr0: "[" ">" tactic_then_gen "]"
0 tactic_expr0: ssrparentacarg
93 tactic_expr0: tactic_atom
682 tactic_expr1: "first" "[" LIST0 tactic_expr SEP "|" "]"
14725 tactic_expr1: "idtac" LIST0 message_token
2573 tactic_expr1: "solve" "[" LIST0 tactic_expr SEP "|" "]"
4216 tactic_expr1: failkw [ int_or_var | ] LIST0 message_token
10013 tactic_expr1: match_key "goal" "with" match_context_list "end"
124 tactic_expr1: match_key "reverse" "goal" "with" match_context_list "end"
7719 tactic_expr1: match_key tactic_expr "with" match_list "end"
645110 tactic_expr1: reference LIST0 tactic_arg_compat
3466513 tactic_expr1: simple_tactic
18290 tactic_expr1: tactic_arg
1023 tactic_expr1: tactic_expr ssrintros_ne
434 tactic_expr2: "tryif" tactic_expr "then" tactic_expr "else" tactic_expr
0 tactic_expr2: tactic_expr "+" binder_tactic
0 tactic_expr2: tactic_expr "+" tactic_expr
31 tactic_expr2: tactic_expr "||" binder_tactic
12710 tactic_expr2: tactic_expr "||" tactic_expr
930 tactic_expr3: "abstract" NEXT
0 tactic_expr3: "abstract" NEXT "using" ident
0 tactic_expr3: "abstract" ssrdgens
775 tactic_expr3: "do" int_or_var ssrmmod ssrdotac ssrclauses
13950 tactic_expr3: "do" int_or_var tactic_expr
62 tactic_expr3: "do" ssrmmod ssrdotac ssrclauses
0 tactic_expr3: "do" ssrortacarg ssrclauses
0 tactic_expr3: "exactly_once" tactic_expr
0 tactic_expr3: "infoH" tactic_expr
31 tactic_expr3: "once" tactic_expr
1891 tactic_expr3: "progress" tactic_expr
25296 tactic_expr3: "repeat" tactic_expr
0 tactic_expr3: "time" OPT string tactic_expr
0 tactic_expr3: "timeout" int_or_var tactic_expr
43989 tactic_expr3: "try" tactic_expr
0 tactic_expr3: selector tactic_expr
0 tactic_expr4: tactic_expr ";" "first" ssr_first_else
341 tactic_expr4: tactic_expr ";" "first" ssrseqarg
93 tactic_expr4: tactic_expr ";" "last" ssrseqarg
1426 tactic_expr4: tactic_expr ";" binder_tactic
1534128 tactic_expr4: tactic_expr ";" tactic_expr
82956 tactic_expr4: tactic_expr ";" tactic_then_locality tactic_then_gen "]"
21297 tactic_expr5: binder_tactic
0 tactic_mode: "par" ":" OPT ltac_info tactic ltac_use_default
2140178 tactic_mode: OPT ltac_selector OPT ltac_info tactic ltac_use_default
186 tactic_mode: OPT toplevel_selector "{"
0 tactic_mode: OPT toplevel_selector G_vernac.query_command
6975 tactic_then_gen:
341 tactic_then_gen: ".." tactic_then_last
10850 tactic_then_gen: "|" tactic_then_gen
75578 tactic_then_gen: tactic_expr
93 tactic_then_gen: tactic_expr ".." tactic_then_last
79329 tactic_then_gen: tactic_expr "|" tactic_then_gen
403 tactic_then_last:
31 tactic_then_last: "|" LIST0 ( OPT tactic_expr ) SEP "|"
82956 tactic_then_locality: "[" OPT ">"
0 test: int_or_var comparison int_or_var
33139 test_lpar_id_colon: local_test_lpar_id_colon
589 thm_token: "Corollary"
558 thm_token: "Fact"
289509 thm_token: "Lemma"
0 thm_token: "Property"
31 thm_token: "Proposition"
186 thm_token: "Remark"
44299 thm_token: "Theorem"
0 toplevel_selector: "!" ":"
62 toplevel_selector: "all" ":"
5146 toplevel_selector: selector_body ":"
4371 type_cstr:
14725 type_cstr: ":" lconstr
8494 type_cstr: OPT [ ":" lconstr ]
93 typeclass_constraint: "!" operconstr200
0 typeclass_constraint: "{" name "}" ":" [ "!" | ] operconstr200
2480 typeclass_constraint: name_colon [ "!" | ] operconstr200
11811 typeclass_constraint: operconstr200
62806 uconstr: constr
249643 unfold_occ: smart_global occs
0 univ_constraint: universe_name [ "<" | "=" | "<=" ] universe_name
0 univ_decl: "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
0 univ_name_list: "@{" LIST0 name "}"
0 universe: "max" "(" LIST1 universe_expr SEP "," ")"
0 universe: universe_expr
0 universe_expr: universe_name universe_increment
0 universe_increment:
0 universe_increment: "+" natural
0 universe_level: "Prop"
0 universe_level: "Set"
0 universe_level: "Type"
0 universe_level: "_"
0 universe_level: global
0 universe_name: "Prop"
0 universe_name: "Set"
0 universe_name: global
95945 var: ident
4030 vernac: "Global" vernac_poly
14601 vernac: "Local" vernac_poly
3826671 vernac: vernac_poly
1209 vernac_aux: "Program" gallina "."
3100 vernac_aux: "Program" gallina_ext "."
808325 vernac_aux: command "."
2140364 vernac_aux: command_entry
522226 vernac_aux: gallina "."
150567 vernac_aux: gallina_ext "."
137082 vernac_aux: subprf
82429 vernac_aux: syntax "."
0 vernac_control: "Fail" vernac_control
0 vernac_control: "Redirect" ne_string vernac_control
0 vernac_control: "Time" vernac_control
0 vernac_control: "Timeout" natural vernac_control
3845302 vernac_control: decorated_vernac
31 vernac_poly: "Monomorphic" vernac_aux
0 vernac_poly: "Polymorphic" vernac_aux
3845271 vernac_poly: vernac_aux
0 vernac_toplevel: "BackTo" natural "."
0 vernac_toplevel: "Drop" "."
0 vernac_toplevel: "Quit" "."
0 vernac_toplevel: Pvernac.Vernac_.main_entry
0 vernac_toplevel: test_show_goal "Show" "Goal" natural "at" natural "."
1585898 with_bindings:
89187 with_bindings: "with" bindings
310 with_declaration: "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr
1085 with_declaration: "Module" fullyqualid ":=" qualid
2759 with_names:
0 with_names: "as" simple_intropattern
1488 withtac:
0 withtac: "with" Tactic.tactic