aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-29 13:43:28 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-29 13:43:28 +0100
commit3624d943513ff1d79fdadf5b231ffcd3786b16c8 (patch)
tree6bfd3884ff693eb7bfe5abd3dfc21c537eb5f1ea /pretyping/typeclasses.mli
parentc0e5746e6b273eb4592d24867da55dde40b656c9 (diff)
parent1e1d8d67442dc3cdd248b7f5e027b9d6bf998ba3 (diff)
Merge PR #6405: Remove the local polymorphic flag hack.
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