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

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

1 files changed, 0 insertions, 7 deletions

diff --git a/lib/future.ml b/lib/future.ml
index 960363e252..77386a1a9f 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 ->