From c81254903e1e50a2305cd48ccfb673d9737afc48 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:52:52 +0000
Subject: get rid of closures in global/proof state

In some cases, an 'a -> 'b field is changed into an ('a -> b') option
field so that one can forget the closures and marshal the resulting
state

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

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index eb5c016922..d95e9fe737 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -139,6 +139,8 @@ let join_safe_environment e =
     {e with future_cst = []} e.future_cst
 
 (* TODO : out of place and maybe incomplete w.r.t. modules *)
+(* this is there to explore the opaque pre-env structure but is
+ * not part of the trusted code base *)
 let prune_env env =
   let env = Environ.pre_env env in
   let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in
-- 
cgit v1.2.3