diff options
| author | Pierre-Marie Pédrot | 2017-07-11 22:49:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-13 15:14:45 +0200 |
| commit | 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 (patch) | |
| tree | 0fd697ed68507449268811a630a201f7637c3553 /API | |
| parent | 9938aed874d3e15e5d21689ea841bdc3e6ebb40e (diff) | |
Make the typeclass implementation fully compatible with universe polymorphism.
This essentially means storing the abstract universe context in the typeclass
data, and abstracting it when necessary.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli index 48fd3a682f..0f3394fe9f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3048,6 +3048,7 @@ end module Typeclasses : sig type typeclass = Typeclasses.typeclass = { + cl_univs : Univ.AUContext.t; cl_impl : Globnames.global_reference; cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t; cl_props : Context.Rel.t; |