Skip to content

Use counts for parser productions

Jim Fehrle edited this page Aug 27, 2019 · 1 revision

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
Clone this wiki locally
You can’t perform that action at this time.