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, 1 insertions, 1 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1c98ec21dd..2970eece8f 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1878,7 +1878,7 @@ let add_morphism_infer glob m n =
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
       in
-      let hook = Future.mk_hook hook in
+      let hook = Lemmas.mk_hook hook in
 	Flags.silently
 	  (fun () ->
 	    Lemmas.start_proof instance_id kind (instance, ctx) hook;