From de26e97cf37cafd37b83377d2df062a6e82676e7 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 12 May 2013 15:33:40 +0000
Subject: Use the Hook module here and there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declaremods.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'library/declaremods.ml')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 894445de1..15a964792 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -600,11 +600,7 @@ let start_library dir =
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
-let end_library_hook = ref ignore
-let set_end_library_hook f = end_library_hook := f
-
 let end_library dir =
-  !end_library_hook();
   let prefix, lib_stack = Lib.end_compilation dir in
   let mp,cenv,ast = Global.export dir in
   let substitute, keep, _ = Lib.classify_segment lib_stack in
-- 
cgit v1.2.3