Classes (coq-core.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

val add_observer : ( Event.t -> unit ) -> unit

Setting opacity

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

For generation on names based on classes only

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