From a91df5fdc60977accd7937eb17b62bd551d3213a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 17 Feb 2015 22:41:26 +0100
Subject: Remove Whelp commands.

Although these commands were never deprecated, they have been unusable for some
time now, since they send requests to an Italian server which is no longer
alive.
---
 ide/MacOS/default_accel_map | 1 -
 ide/coq_commands.ml         | 2 --
 ide/coqide.ml               | 1 -
 ide/coqide_ui.ml            | 1 -
 4 files changed, 5 deletions(-)

(limited to 'ide')

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' />
-- 
cgit v1.2.3