aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.mli')
-rw-r--r--pretyping/typeclasses.mli7
1 files changed, 2 insertions, 5 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2646c09dd..c091842f0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -52,8 +52,8 @@ 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 register_add_instance_hint : (constant -> int option -> unit) -> unit
+val add_instance_hint : constant -> int option -> unit
val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
val is_class : global_reference -> bool
@@ -89,9 +89,6 @@ val nf_substitution : evar_map -> substitution -> substitution
val is_implicit_arg : hole_kind -> bool
-val qualid_of_con : Names.constant -> Libnames.reference
-
-
(* debug *)
(* val subst : *)