From a49cd60c67aca452500c82aad61327823f9abe31 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2015 14:16:19 +0200
Subject: Fixing bug #4234.

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

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2508f4ef3b..6d076ecd11 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -713,7 +713,7 @@ let define_pure_evar_as_product evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
-  let concl = whd_evar evd evi.evar_concl in
+  let concl = whd_betadeltaiota evenv evd evi.evar_concl in
   let s = destSort concl in
   let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
   let evd2,rng =
-- 
cgit v1.2.3