diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/MacOS/default_accel_map | 1 | ||||
| -rw-r--r-- | ide/coq_commands.ml | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 1 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 1 |
4 files changed, 0 insertions, 5 deletions
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 6f474eb124..47612cdf72 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -247,7 +247,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "") ; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "") -; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "") (gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l") ; (gtk_accel_path "<Actions>/Tactics/Tactic right" "") ; (gtk_accel_path "<Actions>/Edit/Find Previous" "<Shift>F3") diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 995c45c5ae..37e38a5464 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -228,8 +228,6 @@ let state_preserving = [ "Test Printing Synth"; "Test Printing Wildcard"; - "Whelp Hint"; - "Whelp Locate"; ] diff --git a/ide/coqide.ml b/ide/coqide.ml index cb05363ddc..4564d620ea 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1171,7 +1171,6 @@ let build_ui () = qitem "About" (Some "<Ctrl><Shift>A"); qitem "Locate" (Some "<Ctrl><Shift>L"); qitem "Print Assumptions" (Some "<Ctrl><Shift>N"); - qitem "Whelp Locate" None; ]; menu tools_menu [ diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index af71b1e78c..edfe28b261 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -119,7 +119,6 @@ let init () = <menuitem action='About' /> <menuitem action='Locate' /> <menuitem action='Print Assumptions' /> - <menuitem action='Whelp Locate' /> </menu> <menu name='Tools' action='Tools'> <menuitem action='Comment' /> |