From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 vernac/search.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'vernac/search.mli')

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} *)
 
-- 
cgit v1.2.3