aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-02 11:33:34 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-06 09:59:01 +0200
commitce11f55e27c8e4f98384aacd61ee67c593340195 (patch)
tree9537fb3faf09eb0bb67eef5a25be7cca2516040a /theories/Structures
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 'theories/Structures')
0 files changed, 0 insertions, 0 deletions