Ajout query Locate dans coqide sur suggestion Arthur C.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11097 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 0 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index aa3bc87fa..3cc85b6f2 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2894,6 +2894,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 								       ())
 					  in
 					  let _ = 
+					    queries_factory#add_item "_Locate" 
+					      ~callback:(fun () -> let term = get_current_word () in
+								     (Command_windows.command_window ())#new_command
+								       ~command:"Locate"
+								       ~term 
+								       ())
+					  in
+					  let _ = 
 					    queries_factory#add_item "_Whelp Locate" 
 					      ~callback:(fun () -> let term = get_current_word () in
 								     (Command_windows.command_window ())#new_command