aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ide.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ide.mllib')
-rw-r--r--ide/ide.mllib7
1 files changed, 6 insertions, 1 deletions
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 83b314283..b2f32fcf7 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -14,8 +14,13 @@ Config_lexer
Utf8_convert
Preferences
Project_file
-Ideutils
+Serialize
+Richprinter
+Xml_lexer
+Xml_parser
+Xml_printer
Xmlprotocol
+Ideutils
Coq
Coq_lex
Sentence