aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-06-02 11:34:10 +0200
committerGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-06-02 11:34:10 +0200
commitabd469790c2e144f693e1b21c5cdc03aee178e6d (patch)
tree7cbcbd2fdce7cab65a3d045da045ea2e21cd510d /ide/coqide.ml
parent2911de377786ad525dd9407968dae7c1973d7190 (diff)
Merge the user queries tab with the shortcut tab.
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8697ca833..d4f47b15e 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>";