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.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'library/keys.ml')

diff --git a/library/keys.ml b/library/keys.ml
index 34a6adab..3cadcb64 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -10,12 +10,13 @@
 
 (** Keys for unification and indexing *)
 
-open Globnames
-open Term
+open Names
+open Constr
 open Libobject
+open Globnames
 
 type key =
-  | KGlob of global_reference
+  | KGlob of GlobRef.t
   | KLam
   | KLet
   | KProd
@@ -126,7 +127,7 @@ let constr_key kind c =
       | Construct (c,u) -> KGlob (ConstructRef c)
       | Var id -> KGlob (VarRef id)
       | App (f, _) -> aux f
-      | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p))
+      | Proj (p, _) -> KGlob (ConstRef (Projection.constant p))
       | Cast (p, _, _) -> aux p
       | Lambda _ -> KLam 
       | Prod _ -> KProd
-- 
cgit v1.2.3