From d05ac62db9ce0715944983e42d3001fa710327e5 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 3 Oct 2013 09:10:59 +0000
Subject: A shallow copy of a pre_env does not contain the vm cache

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16845 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3cde1538d7..57e44a3226 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -207,7 +207,10 @@ let prune_env env =
     { glob with env_constants = Cmap_env.map prune_ckey glob.env_constants }
   in
   let env = Environ.pre_env env in
-  Environ.env_of_pre_env {env with env_globals = prune_globals env.env_globals}
+  Environ.env_of_pre_env {env with
+    env_globals = prune_globals env.env_globals;
+    env_named_vals = [];
+    env_rel_val = []}
 let prune_safe_environment e =
   { e with
     modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE);
-- 
cgit v1.2.3