aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-11 22:49:32 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-13 15:14:45 +0200
commit8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 (patch)
tree0fd697ed68507449268811a630a201f7637c3553 /library/lib.mli
parent9938aed874d3e15e5d21689ea841bdc3e6ebb40e (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 'library/lib.mli')
0 files changed, 0 insertions, 0 deletions