From 0dfaecc2de2306ff9674a4aa3e546d3123015169 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 8 Jun 2014 20:39:58 +0200 Subject: Moving hook code from Future to Lemmas. This seemed to disrupt compilation of the checker, and it was not used before that anyway. --- lib/future.mli | 5 ----- 1 file changed, 5 deletions(-) (limited to 'lib/future.mli') 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. -- cgit v1.2.3