Future: ported to Ephemeron + exception enhancing

A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.

A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost.  This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 22 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 57e44a3226..90d52572a7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -197,28 +197,6 @@ let join_safe_environment e =
     (fun e fc -> add_constraints (Now (Future.join fc)) 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 open Pre_env in
-  let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in
-  let prune_globals glob =
-    { 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;
-    env_named_vals = [];
-    env_rel_val = []}
-let prune_safe_environment e =
-  { e with
-    modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE);
-    revstruct = Modops.prune_structure e.revstruct;
-    future_cst = [];
-    env = prune_env e.env }
-
-
 (** {6 Various checks } *)
 
 let exists_modlabel l senv = Label.Set.mem l senv.modlabels