5 files changed, 10 insertions, 5 deletions
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml
index 20e9f0134f..dc616066c2 100644
--- a/ide/coqide/coq.ml
+++ b/ide/coqide/coq.ml
@@ -538,7 +538,7 @@ struct
 
   let implicit = BoolOpt ["Printing"; "Implicit"]
   let coercions = BoolOpt ["Printing"; "Coercions"]
-  let raw_matching = BoolOpt ["Printing"; "Matching"]
+  let nested_matching = BoolOpt ["Printing"; "Matching"]
   let notations = BoolOpt ["Printing"; "Notations"]
   let parentheses = BoolOpt ["Printing"; "Parentheses"]
   let all_basic = BoolOpt ["Printing"; "All"]
@@ -553,8 +553,8 @@ struct
   let bool_items = [
     { opts = [implicit]; init = false; label = "Display _implicit arguments" };
     { opts = [coercions]; init = false; label = "Display _coercions" };
-    { opts = [raw_matching]; init = true;
-      label = "Display raw _matching expressions" };
+    { opts = [nested_matching]; init = true;
+      label = "Display nested _matching expressions" };
     { opts = [notations]; init = true; label = "Display _notations" };
     { opts = [parentheses]; init = false; label = "Display _parentheses" };
     { opts = [all_basic]; init = false;
diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml
index 6e02d7fed1..3a080d5f51 100644
--- a/ide/coqide/coq_commands.ml
+++ b/ide/coqide/coq_commands.ml
@@ -93,7 +93,6 @@ let commands = [
    ];
   ["Read Module";
    "Record";
-   "Variant";
    "Remark";
    "Remove LoadPath";
    "Remove Printing Constructor";
diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml
index badfabf07e..82eca905ea 100644
--- a/ide/coqide/coqide_ui.ml
+++ b/ide/coqide/coqide_ui.ml
@@ -77,7 +77,7 @@ let init () =
 \n    <separator/>\
 \n    <menuitem action='Display implicit arguments' />\
 \n    <menuitem action='Display coercions' />\
-\n    <menuitem action='Display raw matching expressions' />\
+\n    <menuitem action='Display nested matching expressions' />\
 \n    <menuitem action='Display notations' />\
 \n    <menuitem action='Display parentheses' />\
 \n    <menuitem action='Display all basic low-level contents' />\
diff --git a/ide/coqide/dune b/ide/coqide/dune
index 4bb4672cd4..d2642f77bf 100644
--- a/ide/coqide/dune
+++ b/ide/coqide/dune
@@ -51,6 +51,9 @@
  (modes exe byte)
  (libraries coqide_gui))
 
+(documentation
+ (package coqide))
+
 ; Input-method bindings
 (executable
  (name default_bindings_src)
diff --git a/ide/coqide/index.mld b/ide/coqide/index.mld
new file mode 100644
index 0000000000..8852a2a7eb
--- /dev/null
+++ b/ide/coqide/index.mld
@@ -0,0 +1,3 @@
+{0 coqide }
+
+The coqide package only contains the CoqIDE executable and no OCaml library.