diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-05-16 20:18:02 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-05-16 20:20:25 +0200 |
| commit | 0f6a9c150b1a93358f6e9f8de5072fff52625ab9 (patch) | |
| tree | abf3c9593a4af215a1a334bacfbc78b01543cdba /lib/future.mli | |
| parent | c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2 (diff) | |
Declare: fix Future management
Diffstat (limited to 'lib/future.mli')
| -rw-r--r-- | lib/future.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/future.mli b/lib/future.mli index 09d18ff26..b4eced06a 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -84,6 +84,9 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation the value is not just the 'a but also the global system state *) val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation +(* To get the fix_exn of a computation *) +val fix_exn_of : 'a computation -> fix_exn + (* Run remotely, returns the function to assign. Optionally tekes a function that is called when forced. The default one is to raise NotReady. The assignement function does not change the uuid. *) |