aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-06-13 14:16:49 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-06-22 13:09:16 +0200
commit1311a2bf08ac1deb16f0b3064bc1164d75858a97 (patch)
treeb583fda3032bb363ce85dd621fcd41f7fb9d98f1 /engine
parentd236c7362053c4fc8f1c7f3b59248b412b029fb8 (diff)
Remove hack skipping comparison of algebraic universes in subtyping.
When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions