diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index ee9c83dad3..f8aedf88c2 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -25,33 +25,33 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen (** This module defines type-classes *) type typeclass = { + cl_univs : Univ.AUContext.t; (** The toplevel universe quantification in which the typeclass lives. In particular, [cl_props] and [cl_context] are quantified over it. *) - cl_univs : Univ.AUContext.t; + cl_impl : GlobRef.t; (** The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) - cl_impl : GlobRef.t; + cl_context : GlobRef.t option list * Constr.rel_context; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. *) - cl_context : GlobRef.t option list * Constr.rel_context; - (** Context of definitions and properties on defs, will not be shared *) cl_props : Constr.rel_context; + (** Context of definitions and properties on defs, will not be shared *) + cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; - (** Whether we use matching or full unification during resolution *) cl_strict : bool; + (** Whether we use matching or full unification during resolution *) + cl_unique : bool; (** Whether we can assume that instances are unique, which allows no backtracking and sharing of resolution. *) - cl_unique : bool; } type instance @@ -119,8 +119,8 @@ val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit -val classes_transparent_state_hook : (unit -> transparent_state) Hook.t -val classes_transparent_state : unit -> transparent_state +val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t +val classes_transparent_state : unit -> TransparentState.t val add_instance_hint_hook : (global_reference_or_constr -> GlobRef.t list -> @@ -133,7 +133,10 @@ val remove_instance_hint : GlobRef.t -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : hint_info option -> bool -> 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 declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit (** Build the subinstances hints for a given typeclass object. |