From 4c6c284ddc6db47f070026ad68b5c29f6737c4a0 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 19 May 2011 22:23:33 +0000
Subject: Remove useless "open Gc"

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

(limited to 'lib')

diff --git a/lib/profile.ml b/lib/profile.ml
index 53ba0c19b3..a6e2faa424 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Gc
-
 let word_length = Sys.word_size / 8
 
 let float_of_time t = float_of_int t /. 100.
-- 
cgit v1.2.3