From 020aa7a8e9bca88631e6d7fa68d1ff462f5af25a Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 18 Oct 2013 13:52:10 +0000
Subject: 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
---
 kernel/declareops.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/declareops.mli')

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index f593b45472..177ae9d45e 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -59,7 +59,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 
 val join_constant_body : constant_body -> unit
-val prune_constant_body : constant_body -> constant_body
 
 (** {6 Hash-consing} *)
 
-- 
cgit v1.2.3