From de9798346c7df0593d4d7b83a8f316991f6fb230 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Fri, 30 Aug 2013 12:20:07 +0000 Subject: Stm: if slave process dies badly go back to local lazy evaluation Processing the proof in a slave process may fail for an implementation error, e.g. the state could not be marshalled, or an anomaly is raised by the slave. In this case we fall back to local, lazy, evaluation in the master process. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16743 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/future.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'lib/future.mli') diff --git a/lib/future.mli b/lib/future.mli index 3da0e2fdc..39be0c180 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -19,7 +19,8 @@ val create : (unit -> 'a) -> 'a computation val from_val : 'a -> 'a computation (* Run remotely, returns the function to assign *) -val create_delegate : unit -> 'a computation * ('a value -> unit) +type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] +val create_delegate : unit -> 'a computation * ('a assignement -> unit) (* Variants to stock a copy of the current environment *) val create_here : (unit -> 'a) -> 'a computation -- cgit v1.2.3