diff options
Diffstat (limited to 'lib/future.mli')
| -rw-r--r-- | lib/future.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/lib/future.mli b/lib/future.mli index 8e5f704837..c0fc91bcc3 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -55,10 +55,6 @@ val create : fix_exn -> (unit -> 'a) -> 'a computation argument should really be given *) val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation -(* Like from_val, but also takes a snapshot of the global state. Morally - 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 and build a Lemmas.declaration_hook. * When a future enters the environment a corresponding hook is run to perform * some work. If this fails, then its failure has to be annotated with the @@ -100,9 +96,6 @@ val compute : 'a computation -> 'a value * in a computation obtained by chaining on a joined future. *) val join : 'a computation -> 'a -(* Call this before stocking the future. If it is_val then it is joined *) -val sink : 'a computation -> unit - (*** Utility functions ************************************************* ***) val split2 : ('a * 'b) computation -> 'a computation * 'b computation |