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!).
---
 kernel/modops.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 22f523a9ae..02bab581aa 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
-- 
cgit v1.2.3