aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.mli')
-rw-r--r--pretyping/typeclasses.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 0cbe1c71c..ee28ec173 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -53,7 +53,7 @@ val all_instances : unit -> instance list
val add_class : typeclass -> unit
-val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
global_reference -> instance
val add_instance : instance -> unit
val remove_instance : instance -> unit