diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /parsing/search.mli | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'parsing/search.mli')
-rw-r--r-- | parsing/search.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/parsing/search.mli b/parsing/search.mli index 8ee708bc..7d12d26f 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: search.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: search.mli 11739 2009-01-02 19:33:19Z herbelin $ i*) open Pp open Names @@ -19,13 +19,14 @@ open Nametab (*s Search facilities. *) type glob_search_about_item = - | GlobSearchRef of global_reference + | GlobSearchSubPattern of constr_pattern | 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 : glob_search_about_item list -> dir_path list * bool -> unit +val search_about : + (bool * glob_search_about_item) 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,4 +47,4 @@ 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) -> - glob_search_about_item list -> unit + (bool * glob_search_about_item) list -> unit |