diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-12 19:36:15 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-27 11:52:57 +0100 |
| commit | 05fc0542f6c7a15b9187a2a91beb0aa7a42bb2fa (patch) | |
| tree | 97eccce3247c2d6d79d9b3cde4bc86410bd1d02c /pretyping/typeclasses.mli | |
| parent | 2a25e1a56460556f8b8dcef2a70cd0d2b9422383 (diff) | |
Remove the local polymorphic flag hack.
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 2 |
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 |