diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-03-25 18:29:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:58 +0200 |
| commit | 62fb849cf9410ddc2d9f355570f4fb859f3044c3 (patch) | |
| tree | 2f350ca302a46e18840638d20e7ff89beaf2b1f0 /pretyping/typeclasses.ml | |
| parent | ca318cd0d21ce157a3042b600ded99df6face25e (diff) | |
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index fdcce914d..ada497ece 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -99,7 +99,7 @@ let typeclass_univ_instance (cl,u') = match cl.cl_impl with | ConstRef c -> let cb = Global.lookup_constant c in - if cb.const_polymorphic then Univ.UContext.instance (Future.force cb.const_universes) + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes else Univ.Instance.empty | IndRef c -> let mib,oib = Global.lookup_inductive c in |