diff options
Diffstat (limited to 'parsing/search.mli')
| -rw-r--r-- | parsing/search.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/search.mli b/parsing/search.mli index d1f6bccd48..073a20f87c 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -21,6 +21,7 @@ open Nametab val search_by_head : global_reference -> dir_path list * bool -> unit val search_rewrite : constr_pattern -> dir_path list * bool -> unit val search_pattern : constr_pattern -> dir_path list * bool -> unit +val search_about : global_reference -> dir_path list * bool -> unit (* The filtering function that is by standard search facilities. It can be passed as argument to the raw search functions. |