Moving hook code from Future to Lemmas. This seemed to disrupt compilation of

the checker, and it was not used before that anyway.

2 files changed, 0 insertions, 12 deletions

diff --git a/lib/future.ml b/lib/future.ml
index 960363e25..77386a1a9 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -91,13 +91,6 @@ 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
-type 'a hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
-let mk_hook hook = hook
-let call_hook fix_exn hook l c =
-  try hook l c
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in
-    raise (fix_exn e)
 
 let default_force () = raise NotReady
 let assignement ck = fun v ->
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.