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

---
 library/keys.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'library/keys.mli')

diff --git a/library/keys.mli b/library/keys.mli
index 1fb9a3de..19838365 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Globnames
-
 type key
 
 val declare_equiv_keys : key -> key -> unit
@@ -21,5 +19,5 @@ val equiv_keys : key -> key -> bool
 val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
 (** Compute the head key of a term. *)
 
-val pr_keys : (global_reference -> Pp.t) -> Pp.t
+val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t
 (** Pretty-print the mapping *)
-- 
cgit v1.2.3