summaryrefslogtreecommitdiff
path: root/ide/ide.mllib
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /ide/ide.mllib
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
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