summaryrefslogtreecommitdiff
path: root/ide/ide.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ide.mllib')
-rw-r--r--ide/ide.mllib11
1 files changed, 5 insertions, 6 deletions
diff --git a/ide/ide.mllib b/ide/ide.mllib
index b2f32fcf..96ea8c41 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
@@ -19,6 +14,9 @@ Richprinter
Xml_lexer
Xml_parser
Xml_printer
+Serialize
+Richpp
+Topfmt
Xmlprotocol
Ideutils
Coq
@@ -28,15 +26,16 @@ Gtk_parsing
Wg_Segment
Wg_ProofView
Wg_MessageView
+Wg_RoutedMessageViews
Wg_Detachable
Wg_Find
Wg_Completion
Wg_ScriptView
Coq_commands
-Wg_Command
FileOps
Document
CoqOps
+Wg_Command
Session
Coqide_ui
NanoPG