From 25c82d55497db43bf2cd131f10d2ef366758bbe1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 18 Nov 2016 13:25:05 +0100
Subject: Fix UGraph.check_eq!

Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.

Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.

Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
---
 toplevel/command.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7ffe680e5e..ed3eac51b6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -537,11 +537,9 @@ let inductive_levels env evdref poly arities inds =
 	in
 	let duu = Sorts.univ_of_sort du in
 	let evd =
-	  if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
-	    if is_flexible_sort evd duu then
-	      if Evd.check_leq evd Univ.type0_univ duu then
-	      	evd
-	      else Evd.set_eq_sort env evd (Prop Null) du
+	  if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
+	    if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
+	      Evd.set_eq_sort env evd (Prop Null) du
 	    else evd
 	  else Evd.set_eq_sort env evd (Type cu) du
 	in
-- 
cgit v1.2.3