From f86b7d3b8cb23e2fc19a936accb421bfdbf2cb4d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 12:54:07 +0200
Subject: Fix for a second avatar of bug #4234.

---
 pretyping/evarutil.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6d076ecd11..ee6bbe7fbe 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -795,8 +795,10 @@ let define_evar_as_sort env evd (ev,args) =
   let evd, u = new_univ_variable univ_rigid evd in
   let evi = Evd.find_undefined evd ev in 
   let s = Type u in
+  let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
+  let sort = destSort concl in
   let evd' = Evd.define ev (mkSort s) evd in
-    Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s
+  Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
 
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
-- 
cgit v1.2.3