Module Classes

val declare_instance : ?⁠warn:bool -> Environ.env -> Evd.evar_map -> Typeclasses.hint_info option -> Hints.hint_locality -> Names.GlobRef.t -> unit

Declares the given global reference as an instance of its type. Does nothing — or emit a “not-a-class” warning if the warn argument is set — when said type is not a registered type class.

val existing_instance : ?⁠loc:Loc.t -> Hints.hint_locality -> Names.GlobRef.t -> Vernacexpr.hint_info_expr option -> unit

globality, reference, optional priority and pattern information

val new_instance_interactive : locality:Hints.hint_locality -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> ?⁠tac:unit Proofview.tactic -> ?⁠hook:(Names.GlobRef.t -> unit) -> Vernacexpr.hint_info_expr -> (bool * Constrexpr.constr_expr) option -> Names.Id.t * Declare.Proof.t
val new_instance : locality:Hints.hint_locality -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> (bool * Constrexpr.constr_expr) -> ?⁠hook:(Names.GlobRef.t -> unit) -> Vernacexpr.hint_info_expr -> Names.Id.t
val new_instance_program : locality:Hints.hint_locality -> pm:Declare.OblState.t -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> (bool * Constrexpr.constr_expr) option -> ?⁠hook:(Names.GlobRef.t -> unit) -> Vernacexpr.hint_info_expr -> Declare.OblState.t * Names.Id.t
val declare_new_instance : locality:Hints.hint_locality -> program_mode:bool -> poly:bool -> Constrexpr.ident_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Vernacexpr.hint_info_expr -> unit
val add_class : Typeclasses.typeclass -> unit
type instance = {
class_name : Names.GlobRef.t;
instance : Names.GlobRef.t;
info : Typeclasses.hint_info;
locality : Hints.hint_locality;
}
module Event : sig ... end
type observer
val register_observer : name:string -> ?⁠override:bool -> (Event.t -> unit) -> observer
val activate_observer : observer -> unit
val deactivate_observer : observer -> unit
val set_typeclass_transparency : locality:Hints.hint_locality -> Tacred.evaluable_global_reference list -> bool -> unit
val tc_transparency_locality : Hints.hint_locality Attributes.attribute
val set_typeclass_transparency_com : locality:Hints.hint_locality -> Libnames.qualid list -> bool -> unit
val id_of_class : Typeclasses.typeclass -> Names.Id.t
val refine_att : bool Attributes.attribute
val instance_locality : Hints.hint_locality Attributes.attribute
module Internal : sig ... end