From 24d0027f0344bca7abce3b8fa8c2a1e42ecf1a00 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 13 Sep 2014 10:44:40 +0200
Subject: Providing a -type-in-type option for collapsing the universe
 hierarchy.

---
 pretyping/evarconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d125a799b..47955e8e0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -679,7 +679,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	       let evd' =
 		 if pbty == CONV
 		 then Evd.set_eq_sort evd s1 s2
-		 else Evd.set_leq_sort evd s1 s2
+		 else Evd.set_leq_sort env evd s1 s2
 	       in Success evd'
 	     with Univ.UniverseInconsistency p ->
                UnifFailure (evd,UnifUnivInconsistency p)
-- 
cgit v1.2.3