aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
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.ml
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.ml')
0 files changed, 0 insertions, 0 deletions