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

1 files changed, 4 insertions, 1 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3cde1538d..57e44a322 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);