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.

---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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;
-- 
cgit v1.2.3