diff options
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index f231c7406..c06006ad0 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames open Decl_kinds open Term open Sign @@ -41,8 +42,8 @@ type typeclass = { type instance = { is_class: typeclass; - is_name: identifier; (* Name of the instance *) - is_impl: constant; + is_pri : int option; + is_impl: constant; } val instances : Libnames.reference -> instance list @@ -50,6 +51,9 @@ val typeclasses : unit -> typeclass list val add_class : typeclass -> unit val add_instance : instance -> unit +val register_add_instance_hint : (reference -> int option -> unit) -> unit +val add_instance_hint : reference -> int option -> unit + val class_info : identifier -> typeclass (* raises Not_found *) val class_of_inductive : inductive -> typeclass (* raises Not_found *) @@ -75,3 +79,10 @@ val substitution_of_named_context : val nf_substitution : evar_map -> substitution -> substitution val is_implicit_arg : hole_kind -> bool + + +val subst : 'a * Mod_subst.substitution * + ((Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t) -> + (Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t + +val qualid_of_con : Names.constant -> Libnames.reference |