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

---
 interp/reserve.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/reserve.ml')

diff --git a/interp/reserve.ml b/interp/reserve.ml
index 36005121..071248f0 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -22,7 +22,7 @@ open Notation_ops
 open Globnames
 
 type key =
-  | RefKey of global_reference
+  | RefKey of GlobRef.t
   | Oth
 
 (** TODO: share code from Notation *)
@@ -112,7 +112,9 @@ let revert_reserved_type t =
     let t = EConstr.Unsafe.to_constr t in
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
     let t = EConstr.of_constr t in
-    let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
+    let env = Global.env () in
+    let evd = Evd.from_env env in
+    let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =
-- 
cgit v1.2.3