package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a hint_info_gen = {
  1. hint_priority : int option;
  2. hint_pattern : 'a option;
}
type class_method = {
  1. meth_name : Names.Name.t;
  2. meth_info : hint_info option;
  3. meth_const : Names.Constant.t option;
}
type typeclass = {
  1. cl_univs : Univ.AUContext.t;
  2. cl_impl : Names.GlobRef.t;
  3. cl_context : Constr.rel_context;
  4. cl_props : Constr.rel_context;
  5. cl_projs : class_method list;
  6. cl_strict : bool;
  7. cl_unique : bool;
}
type instance = {
  1. is_class : Names.GlobRef.t;
  2. is_info : hint_info;
  3. is_global : int option;
  4. is_impl : Names.GlobRef.t;
}
val instances : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> instance list
val typeclasses : unit -> typeclass list
val all_instances : unit -> instance list
val load_class : typeclass -> unit
val load_instance : instance -> unit
val remove_instance : instance -> unit
val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
val instance_impl : instance -> Names.GlobRef.t
val hint_priority : instance -> int option
val is_class : Names.GlobRef.t -> bool
val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> EConstr.t option * EConstr.t
type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
val all_evars : evar_filter
val all_goals : evar_filter
val no_goals : evar_filter
val no_goals_or_obligations : evar_filter
val make_unresolvables : (Evar.t -> bool) -> Evd.evar_map -> Evd.evar_map
val is_class_evar : Evd.evar_map -> Evd.evar_info -> bool
val is_class_type : Evd.evar_map -> EConstr.types -> bool
val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map
val resolve_one_typeclass : ?unique:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.constr
val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
val classes_transparent_state : unit -> TransparentState.t
val solve_all_instances_hook : (Environ.env -> Evd.evar_map -> evar_filter -> bool -> bool -> bool -> Evd.evar_map) Hook.t
val solve_one_instance_hook : (Environ.env -> Evd.evar_map -> EConstr.types -> bool -> Evd.evar_map * EConstr.constr) Hook.t