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.ml | |
| parent | c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2 (diff) | |
Declare: fix Future management
Diffstat (limited to 'lib/future.ml')
| -rw-r--r-- | lib/future.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/future.ml b/lib/future.ml index 690255edd..77386a1a9 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -90,6 +90,8 @@ let uuid kx = let id, _, _ = get kx in id let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None)) let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ()))) +let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn + let default_force () = raise NotReady let assignement ck = fun v -> let _, fix_exn, c = get ck in |