From abd469790c2e144f693e1b21c5cdc03aee178e6d Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Thu, 2 Jun 2016 11:34:10 +0200
Subject: Merge the user queries tab with the shortcut tab.

---
 ide/coqide.ml      | 1 -
 ide/preferences.ml | 7 +++----
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8697ca8333..d4f47b15e5 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1132,7 +1132,6 @@ let build_ui () =
     qitem "About" (Some "<Ctrl><Shift>A");
     qitem "Locate" (Some "<Ctrl><Shift>L");
     qitem "Print Assumptions" (Some "<Ctrl><Shift>N");
-    qitem "Show Proof" (Some "<Ctrl><Shift>R");
   ];
   user_queries_items queries_menu "Query" user_queries#get "<Ctrl><Shift>";
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index b39a1106c2..6bb19c6389 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -976,11 +976,10 @@ let configure ?(apply=(fun () -> ())) () =
 	     [automatic_tactics]);
      Section("Shortcuts", Some `PREFERENCES,
 	     [modifiers_valid; modifier_for_tactics;
-	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
+        modifier_for_templates; modifier_for_display; modifier_for_navigation;
+        user_queries]);
      Section("Misc", Some `ADD,
-       misc);
-     Section("User queries", None,
-       [user_queries])]
+       misc)]
   in
 (*
   Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font);
-- 
cgit v1.2.3