summaryrefslogtreecommitdiff
path: root/ide/ide.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ide.mllib')
-rw-r--r--ide/ide.mllib23
1 files changed, 23 insertions, 0 deletions
diff --git a/ide/ide.mllib b/ide/ide.mllib
new file mode 100644
index 00000000..63935db3
--- /dev/null
+++ b/ide/ide.mllib
@@ -0,0 +1,23 @@
+Okey
+Config_file
+Configwin_keys
+Configwin_types
+Configwin_messages
+Configwin_ihm
+Configwin
+Editable_cells
+Config_parser
+Tags
+Typed_notebook
+Config_lexer
+Utf8_convert
+Preferences
+Ideutils
+Coq_lex
+Gtk_parsing
+Undo
+Coq
+Coq_commands
+Coq_tactics
+Command_windows
+Coqide