Module Classes

Errors

val mismatched_params : Environ.env -> Constrexpr.constr_expr list -> Constr.rel_context -> 'a
val mismatched_props : Environ.env -> Constrexpr.constr_expr list -> Constr.rel_context -> 'a
val existing_instance : bool -> Libnames.qualid -> Hints.hint_info_expr option -> unit

globality, reference, optional priority and pattern information

val declare_instance_constant : Typeclasses.typeclass -> Hints.hint_info_expr -> bool -> Impargs.manual_explicitation list -> ?⁠hook:(Names.GlobRef.t -> unit) -> Names.Id.t -> UState.universe_decl -> bool -> Evd.evar_map -> Constr.t -> Constr.types -> unit
val new_instance : pstate:Proof_global.t option -> ?⁠global:bool -> ?⁠refine:bool -> program_mode:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> Vernacexpr.typeclass_constraint -> (bool * Constrexpr.constr_expr) option -> ?⁠generalize:bool -> ?⁠tac:unit Proofview.tactic -> ?⁠hook:(Names.GlobRef.t -> unit) -> Hints.hint_info_expr -> Names.Id.t * Proof_global.t option
val declare_new_instance : ?⁠global:bool -> program_mode:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> (Constrexpr.ident_decl * Decl_kinds.binding_kind * Constrexpr.constr_expr) -> Hints.hint_info_expr -> unit
val set_typeclass_transparency : Names.evaluable_global_reference -> bool -> bool -> unit
val id_of_class : Typeclasses.typeclass -> Names.Id.t
val context : pstate:Proof_global.t option -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> bool

returns false if, for lack of section, it declares an assumption (unless in a module type).