From 105db906ae45e792d1caeeb2e3fb7f69944b2caa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 12:53:41 +0200
Subject: - Fixes for canonical structure resolution (check that the initial
 term indeed unifies with the projected term, keeping track of universes). -
 Fix the [unify] tactic to fail properly. - Fix unification to disallow
 lowering a global Type(i) universe to Prop or Set.

---
 pretyping/evd.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'pretyping/evd.ml')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d185685005..166bab4b82 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -390,19 +390,20 @@ let process_universe_constraints univs vars alg local cstrs =
 		  instantiate_variable l' (Univ.Universe.make r') vars
 		else if rloc then 
 		  instantiate_variable r' (Univ.Universe.make l') vars
-		else 
-		  (* Two rigid/global levels, one of them being Prop/Set, disallow *)
-		  (* if Univ.is_small_univ l' || Univ.is_small_univ r' then *)
-		  (*   raise UniversesDiffer *)
-		  (* else *)
-		  if fo then 
-		    if not (Univ.check_eq univs l r) then 
+		else if not (Univ.check_eq univs l r) then
+		  (* Two rigid/global levels, none of them being local,
+		     one of them being Prop/Set, disallow *)
+		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
+		    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, []))
+		  else
+		    if fo then 
 		      raise UniversesDiffer
 	      in
 	        Univ.enforce_eq_level l' r' local
            | _, _ (* One of the two is algebraic or global *) -> 
 	     if Univ.check_eq univs l r then local
-	     else raise UniversesDiffer
+	     else 
+	       raise UniversesDiffer
   in
   let local = 
     Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
-- 
cgit v1.2.3