From ceb68d1d643ac65f500e0201f61e73cf22e6e2fb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 21 Sep 2016 14:11:59 +0200
Subject: Removing dead code in CoqIDE.

There was a pile of dead code inherited from Cameleon just sitting around and
not used at all. This code was introduced in 2003 and never actually used.
---
 ide/ide.mllib | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'ide/ide.mllib')

diff --git a/ide/ide.mllib b/ide/ide.mllib
index b2f32fcf7..72a14134b 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -1,12 +1,7 @@
 Minilib
-Okey
-Config_file
-Configwin_keys
-Configwin_types
 Configwin_messages
 Configwin_ihm
 Configwin
-Editable_cells
 Config_parser
 Tags
 Wg_Notebook
-- 
cgit v1.2.3