diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:34:10 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:34:10 +0200 |
| commit | abd469790c2e144f693e1b21c5cdc03aee178e6d (patch) | |
| tree | 7cbcbd2fdce7cab65a3d045da045ea2e21cd510d /ide | |
| parent | 2911de377786ad525dd9407968dae7c1973d7190 (diff) | |
Merge the user queries tab with the shortcut tab.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 1 | ||||
| -rw-r--r-- | ide/preferences.ml | 7 |
2 files changed, 3 insertions, 5 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>"; diff --git a/ide/preferences.ml b/ide/preferences.ml index b39a1106c..6bb19c638 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); |