diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
| commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
| tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /vernac/search.mli | |
| parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
| parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) | |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
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} *) |