From 1311a2bf08ac1deb16f0b3064bc1164d75858a97 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Jun 2018 14:16:49 +0200 Subject: 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!). --- vernac/himsg.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'vernac') diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5d671ef52..534e58f9c 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -871,9 +871,6 @@ let explain_not_match_error = function pr_enum (function Name id -> Id.print id | _ -> str "_") nal | NotEqualInductiveAliases -> str "Aliases to inductive types do not match" - | NoTypeConstraintExpected -> - strbrk "a definition whose type is constrained can only be subtype " ++ - strbrk "of a definition whose type is itself constrained" | CumulativeStatusExpected b -> let status b = if b then str"cumulative" else str"non-cumulative" in str "a " ++ status b ++ str" declaration was expected, but a " ++ -- cgit v1.2.3