diff options
Diffstat (limited to 'parsing/search.mli')
| -rw-r--r-- | parsing/search.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/parsing/search.mli b/parsing/search.mli index 260c12e9d..851e6431d 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -18,16 +18,15 @@ open Nametab (*s Search facilities. *) -type 'a search_about_item = - | SearchRef of 'a - | SearchString of string +type glob_search_about_item = + | GlobSearchRef of global_reference + | GlobSearchString of string 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 search_about_item list -> - dir_path list * bool -> unit -val search_named : string list -> dir_path list * bool -> unit +val search_about : glob_search_about_item list -> dir_path list * bool -> unit +val search_named : string list -> 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. @@ -46,6 +45,6 @@ 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 search_about_item list -> unit + glob_search_about_item list -> unit val raw_search_named : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> string list -> unit |