diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-13 14:16:49 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-22 13:09:16 +0200 |
| commit | 1311a2bf08ac1deb16f0b3064bc1164d75858a97 (patch) | |
| tree | b583fda3032bb363ce85dd621fcd41f7fb9d98f1 /kernel/modops.ml | |
| parent | d236c7362053c4fc8f1c7f3b59248b412b029fb8 (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 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 22f523a9a..02bab581a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -47,7 +47,6 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types |