diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 12:20:07 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 12:20:07 +0000 |
| commit | de9798346c7df0593d4d7b83a8f316991f6fb230 (patch) | |
| tree | 3541e5bfc7127f14a3a789c0076776c3d0917e9b /lib/future.mli | |
| parent | e458f2e2beb65e49c4bb45c54ab07ce3b0b8a9bb (diff) | |
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
Diffstat (limited to 'lib/future.mli')
| -rw-r--r-- | lib/future.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 |