Use counts for parser productions
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
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.