diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:23:58 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 16:23:58 +0000 |
| commit | cb7cf50289fbf1c5fe60fd915f63128c88dc6d68 (patch) | |
| tree | 4d60e3ef2cf99c0cdc14e190db378e285494a57f | |
| parent | 557df731a4ad524ebabf78359f950ae063ecef51 (diff) | |
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
| -rw-r--r-- | parsing/search.ml | 9 | ||||
| -rw-r--r-- | parsing/search.mli | 2 |
2 files changed, 8 insertions, 3 deletions
diff --git a/parsing/search.ml b/parsing/search.ml index 831c7e13e..74cdd77dd 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 073a20f87..f7e384e96 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 |