summaryrefslogtreecommitdiff
path: root/ide/ide.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ide.mllib')
-rw-r--r--ide/ide.mllib9
1 files changed, 7 insertions, 2 deletions
diff --git a/ide/ide.mllib b/ide/ide.mllib
index e082bd18..b2f32fcf 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,18 +9,23 @@ Configwin
Editable_cells
Config_parser
Tags
-Wg_Segment
Wg_Notebook
Config_lexer
Utf8_convert
Preferences
Project_file
-Ideutils
+Serialize
+Richprinter
+Xml_lexer
+Xml_parser
+Xml_printer
Xmlprotocol
+Ideutils
Coq
Coq_lex
Sentence
Gtk_parsing
+Wg_Segment
Wg_ProofView
Wg_MessageView
Wg_Detachable