diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e4db68fbcd..a00d23a9b2 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -34,8 +34,9 @@ type typeclass = { (** 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 boolean indicates subclasses. *) - cl_projs : (name * bool * constant option) list; + no name is provided. The [int option option] indicates subclasses whose hint has + the given priority. *) + cl_projs : (name * int option option * constant option) list; } type instance @@ -93,10 +94,20 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u val register_classes_transparent_state : (unit -> transparent_state) -> unit val classes_transparent_state : unit -> transparent_state -val register_add_instance_hint : (global_reference -> bool (* local? *) -> int option -> unit) -> unit +val register_add_instance_hint : (constr -> bool (* local? *) -> int option -> unit) -> unit val register_remove_instance_hint : (global_reference -> unit) -> unit -val add_instance_hint : global_reference -> bool -> int option -> unit +val add_instance_hint : constr -> bool -> int option -> unit val remove_instance_hint : global_reference -> unit val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref + +val declare_instance : int option -> bool -> global_reference -> unit + + +(** Build the subinstances hints for a given typeclass object. + check tells if we should check for existence of the + subinstances and add only the missing ones. *) + +val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) -> + (int option * constr) list |