aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ide.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ide.mllib')
-rw-r--r--ide/ide.mllib4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 9bbf9b0d9..ee498ba0c 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,7 +9,7 @@ Configwin
Editable_cells
Config_parser
Tags
-Typed_notebook
+Wg_Notebook
Config_lexer
Utf8_convert
Preferences
@@ -21,6 +21,6 @@ Gtk_parsing
Undo
Coq
Coq_commands
-Command_windows
+Wg_Command
Coqide_ui
Coqide