coq 8.7.2 · OCaml Package

exception Bound

val decompose_app_bound : 
  Evd.evar_map ->
  EConstr.constr ->
  Globnames.global_reference * EConstr.constr array

type debug =

| Debug
| Info
| Off

val secvars_of_hyps : ('c, 't) Context.Named.pt -> Names.Id.Pred.t

val empty_hint_info : 'a Vernacexpr.hint_info_gen

type !'a hint_ast =

| Res_pf of 'a
| ERes_pf of 'a
| Give_exact of 'a
| Res_pf_THEN_trivial_fail of 'a
| Unfold_nth of Names.evaluable_global_reference
| Extern of Genarg.glob_generic_argument

type hint

type raw_hint = EConstr.constr * EConstr.types * Univ.universe_context_set

type !'a hints_path_atom_gen =

| PathHints of 'a list
| PathAny

type hints_path_atom = Globnames.global_reference hints_path_atom_gen

type hint_db_name = string

type !'a with_metadata = private {

pri : int;
poly : Decl_kinds.polymorphic;
pat : Pattern.constr_pattern option;
name : hints_path_atom;
db : hint_db_name option;
secvars : Names.Id.Pred.t;
code : 'a;

}

type full_hint = hint with_metadata

type search_entry

type hint_entry

type !'a hints_path_gen =

| PathAtom of 'a hints_path_atom_gen
| PathStar of 'a hints_path_gen
| PathSeq of 'a hints_path_gen * 'a hints_path_gen
| PathOr of 'a hints_path_gen * 'a hints_path_gen
| PathEmpty
| PathEpsilon

type pre_hints_path = Libnames.reference hints_path_gen

type hints_path = Globnames.global_reference hints_path_gen

val normalize_path : hints_path -> hints_path

val path_matches : hints_path -> hints_path_atom list -> bool

val path_derivate : hints_path -> hints_path_atom -> hints_path

val pp_hints_path_gen : 
  ('a -> Pp.std_ppcmds) ->
  'a hints_path_gen ->
  Pp.std_ppcmds

val pp_hints_path_atom : 
  ('a -> Pp.std_ppcmds) ->
  'a hints_path_atom_gen ->
  Pp.std_ppcmds

val pp_hints_path : hints_path -> Pp.std_ppcmds

val pp_hint_mode : Vernacexpr.hint_mode -> Pp.std_ppcmds

val glob_hints_path_atom : 
  Libnames.reference hints_path_atom_gen ->
  Globnames.global_reference hints_path_atom_gen

val glob_hints_path : 
  Libnames.reference hints_path_gen ->
  Globnames.global_reference hints_path_gen

module Hint_db : sig ... end

type hint_db = Hint_db.t

type hnf = bool

type hint_info =
  (Misctypes.patvar list * Pattern.constr_pattern) Vernacexpr.hint_info_gen

type hint_term =

| IsGlobRef of Globnames.global_reference
| IsConstr of EConstr.constr * Univ.universe_context_set

type hints_entry =

| HintsResolveEntry of (hint_info * Decl_kinds.polymorphic * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * Decl_kinds.polymorphic * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of Names.evaluable_global_reference list
| HintsTransparencyEntry of Names.evaluable_global_reference list * bool
| HintsModeEntry of Globnames.global_reference * Vernacexpr.hint_mode list
| HintsExternEntry of hint_info * Genarg.glob_generic_argument

val searchtable_map : hint_db_name -> hint_db

val searchtable_add : (hint_db_name * hint_db) -> unit

val create_hint_db : 
  bool ->
  hint_db_name ->
  Names.transparent_state ->
  bool ->
  unit

val remove_hints : 
  bool ->
  hint_db_name list ->
  Globnames.global_reference list ->
  unit

val current_db_names : unit -> Util.String.Set.t

val current_pure_db : unit -> hint_db list

val interp_hints : 
  Decl_kinds.polymorphic ->
  Vernacexpr.hints_expr ->
  hints_entry

val add_hints : 
  Vernacexpr.locality_flag ->
  hint_db_name list ->
  hints_entry ->
  unit

val prepare_hint : 
  bool ->
  (bool * bool) ->
  Environ.env ->
  Evd.evar_map ->
  (Evd.evar_map * EConstr.constr) ->
  hint_term

val make_exact_entry : 
  Environ.env ->
  Evd.evar_map ->
  hint_info ->
  Decl_kinds.polymorphic ->
  ?name:hints_path_atom ->
  (EConstr.constr * EConstr.types * Univ.universe_context_set) ->
  hint_entry

val make_apply_entry : 
  Environ.env ->
  Evd.evar_map ->
  (bool * bool * bool) ->
  hint_info ->
  Decl_kinds.polymorphic ->
  ?name:hints_path_atom ->
  (EConstr.constr * EConstr.types * Univ.universe_context_set) ->
  hint_entry

val make_resolves : 
  Environ.env ->
  Evd.evar_map ->
  (bool * bool * bool) ->
  hint_info ->
  Decl_kinds.polymorphic ->
  ?name:hints_path_atom ->
  hint_term ->
  hint_entry list

val make_resolve_hyp : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.named_declaration ->
  hint_entry list

val make_extern : 
  int ->
  Pattern.constr_pattern option ->
  Genarg.glob_generic_argument ->
  hint_entry

val run_hint : 
  hint ->
  ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) ->
  'r Proofview.tactic

val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast

val make_local_hint_db : 
  Environ.env ->
  Evd.evar_map ->
  ?ts:Names.transparent_state ->
  bool ->
  Tactypes.delayed_open_constr list ->
  hint_db

val make_db_list : hint_db_name list -> hint_db list

val typeclasses_db : hint_db_name

val rewrite_db : hint_db_name

val pr_searchtable : unit -> Pp.std_ppcmds

val pr_applicable_hint : unit -> Pp.std_ppcmds

val pr_hint_ref : Globnames.global_reference -> Pp.std_ppcmds

val pr_hint_db_by_name : hint_db_name -> Pp.std_ppcmds

val pr_hint_db : Hint_db.t -> Pp.std_ppcmds

val pr_hint : hint -> Pp.std_ppcmds

val add_hints_init : (unit -> unit) -> unit

package coq