4 files changed, 9 insertions, 10 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/idetop.ml b/ide/coqide/idetop.ml
index 72b54d329f..0a0b932c46 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -489,11 +489,11 @@ let eval_call c =
 let print_xml =
   let m = Mutex.create () in
   fun oc xml ->
-    Mutex.lock m;
-    if !Flags.xml_debug then
-      Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml);
-    try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m
-    with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e
+    CThread.with_lock m ~scope:(fun () ->
+        if !Flags.xml_debug then
+          Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml);
+        try Control.protect_sigalrm (Xml_printer.print oc) xml
+        with e -> let e = Exninfo.capture e in Exninfo.iraise e)
 
 let slave_feeder fmt xml_oc msg =
   let xml = Xmlprotocol.(of_feedback fmt msg) in