From 9ed2a16fb97e7c0c10c12a5fc8eda966b8aa9b22 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 22 Oct 2003 11:18:20 +0000
Subject: Integration de SearchNamed dans SearchAbout

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4698 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/centaur.ml4 | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index a7bd150532..4290eca610 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -550,12 +550,16 @@ let solve_hook n =
 
 let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
 
+let interp_search_about_item = function
+  | SearchRef qid -> SearchRef (Nametab.global qid)
+  | SearchString s as x -> x
+
 let pcoq_search s l =
   ctv_SEARCH_LIST:=[];
   begin match s with
-  | SearchAbout locqid -> 
+  | SearchAbout sl -> 
       raw_search_about (filter_by_module_from_list l) add_search
-	(Nametab.global locqid)
+	(List.map interp_search_about_item sl)
   | SearchPattern c ->
       let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
       raw_pattern_search (filter_by_module_from_list l) add_search pat
-- 
cgit v1.2.3