From 1fdc02ef7bf0b3d98eb2c69ab5cf8cd84f77b668 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Apr 2021 20:22:31 +0200
Subject: Fixes #11690: wrongly toggled coqide printing matching flag; moving
 raw->nested.

---
 ide/coqide/coq.ml       | 6 +++---
 ide/coqide/coqide_ui.ml | 2 +-
 2 files changed, 4 insertions(+), 4 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/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' />\
-- 
cgit v1.2.3