From cb7cf50289fbf1c5fe60fd915f63128c88dc6d68 Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 22 Jan 2003 16:23:58 +0000
Subject: I changed the interface to make sure SearchAbout is defined according
 to the same design pattern as the other search commands.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3588 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/search.ml  | 9 ++++++---
 parsing/search.mli | 2 ++
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/parsing/search.ml b/parsing/search.ml
index 831c7e13ea..74cdd77dd7 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -222,13 +222,16 @@ let gen_filtered_search filter_function display_function =
   gen_crible 
     (fun s a c -> if filter_function s a c then display_function s a c) 
 
-let search_about ref inout =
+let raw_search_about filter_modules display_function ref =
   let c = constr_of_reference ref in
-  let filter_modules = filter_by_module_from_list inout in
   let filter ref' env typ =
     filter_modules ref' env typ &&
     Termops.occur_term c typ
   in
-  gen_filtered_search filter plain_display
+  gen_filtered_search filter display_function
+
+let search_about ref inout = 
+  raw_search_about (filter_by_module_from_list inout) plain_display ref
+
 
 
diff --git a/parsing/search.mli b/parsing/search.mli
index 073a20f87c..f7e384e96b 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -38,3 +38,5 @@ val raw_pattern_search : (global_reference -> env -> constr -> bool) ->
   (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
 val raw_search_rewrite : (global_reference -> env -> constr -> bool) ->
   (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
+val raw_search_about : (global_reference -> env -> constr -> bool) ->
+  (global_reference -> env -> constr -> unit) -> global_reference -> unit
-- 
cgit v1.2.3