Classes
Instance declaration
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
Activated observers are called whenever a class or an instance are declared.
register_observer
is to be called once per process for a given string, unless override
is true
. The registered observer is not activated.
Activation state is part of the summary. It is up to the caller to use libobject for persistence if desired.
val activate_observer : observer -> unit
val deactivate_observer : observer -> 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