diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
| commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
| tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /vernac/search.mli | |
| parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) | |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'vernac/search.mli')
| -rw-r--r-- | vernac/search.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/search.mli b/vernac/search.mli index a1fb7ed3..0dc82c1c 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -12,7 +12,6 @@ open Names open Constr open Environ open Pattern -open Globnames (** {6 Search facilities. } *) @@ -20,8 +19,8 @@ type glob_search_about_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string -type filter_function = global_reference -> env -> constr -> bool -type display_function = global_reference -> env -> constr -> unit +type filter_function = GlobRef.t -> env -> constr -> bool +type display_function = GlobRef.t -> env -> constr -> unit (** {6 Generic filter functions} *) |