diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-08 20:39:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-08 20:53:51 +0200 |
| commit | 0dfaecc2de2306ff9674a4aa3e546d3123015169 (patch) | |
| tree | d031ad991f690c7fa1f77213dcc8af0a9df27a0c /lib/future.mli | |
| parent | 2fceefe036f5f8289fd4667ade8b3240a11579d7 (diff) | |
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
the checker, and it was not used before that anyway.
Diffstat (limited to 'lib/future.mli')
| -rw-r--r-- | lib/future.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/lib/future.mli b/lib/future.mli index 41f5e185c..c4b55db25 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -91,11 +91,6 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation * is split into two parts, the lazy one (the future) and the eagher one * (the hook), both performing some computations for the same state id. *) val fix_exn_of : 'a computation -> fix_exn -type 'a hook -val mk_hook : - (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a hook -val call_hook : - fix_exn -> 'a hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a (* Run remotely, returns the function to assign. Optionally tekes a function that is called when forced. The default one is to raise NotReady. |