From 767839754f9fda66ea6076ddb8939618572bd1d1 Mon Sep 17 00:00:00 2001
From: glondu
Date: Sun, 31 Oct 2010 14:05:47 +0000
Subject: Remove some unnecessary (?) "open Ideutils"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13589 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/gtk_parsing.ml | 2 --
 ide/undo.ml        | 1 -
 2 files changed, 3 deletions(-)

diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 39cf14d3af..c69f92e2dd 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Ideutils
-
 
 let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
 let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)
diff --git a/ide/undo.ml b/ide/undo.ml
index 1b6beeb243..917fc88160 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open GText
-open Ideutils
 type action =
   | Insert of string * int * int (* content*pos*length *)
   | Delete of string * int * int (* content*pos*length *)
-- 
cgit v1.2.3