From 592151e323036f0044a0ac285b8b13c964825989 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Sep 2015 14:06:38 +0200
Subject: Fixing bug #4347: Not_found Exception with some Records.

A term was reduced in an improper environment.
---
 pretyping/evarutil.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ee6bbe7fbe..8ebb037c24 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -757,7 +757,7 @@ let define_evar_as_product evd (evk,args) =
 let define_pure_evar_as_lambda env evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let typ = whd_betadeltaiota env evd (evar_concl evi) in
+  let typ = whd_betadeltaiota evenv evd (evar_concl evi) in
   let evd1,(na,dom,rng) = match kind_of_term typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
-- 
cgit v1.2.3


From b6d5a9f47634371aa18c6e3159c6bc24203d229f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Sep 2015 14:22:29 +0200
Subject: Fixing loss of extra data in Evd.

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

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index fc4f5e040e..6326112912 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1385,7 +1385,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   principal_future_goal = evd.principal_future_goal;
-  extras = Store.empty;
+  extras = evd.extras;
 }
 
 let meta_list evd = metamap_to_list evd.metas
-- 
cgit v1.2.3