From a17f7ecc5e80fc471f330d673ba28a6cb06bcdc7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2008 20:18:29 +0000
Subject: 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
---
 ide/coqide.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index aa3bc87fa8..3cc85b6f26 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2893,6 +2893,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 								       ~term 
 								       ())
 					  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
-- 
cgit v1.2.3