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.

---
 intf/tacexpr.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7895ddbf47..530213b7cf 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -272,5 +272,3 @@ type raw_tactic_arg =
 
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
 type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
-
-type 'a declaration_hook = 'a Future.hook
-- 
cgit v1.2.3