diff options
| -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 |