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(-)

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