aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-05-02 11:33:34 +0200
committerMatthieu Sozeau2014-05-06 09:59:01 +0200
commitce11f55e27c8e4f98384aacd61ee67c593340195 (patch)
tree9537fb3faf09eb0bb67eef5a25be7cca2516040a /dev
parentaf533645b1033dc386d8ac99cc8c4b6491b0ca91 (diff)
Fix extraction taking a type in the wrong environment.
Fix restriction of universe contexts to not forget about potentially useful constraints.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions