From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 3 May 2018 17:44:34 +0200
Subject: Remove some occurrences of Evd.empty

We address the easy ones, but they should probably be all removed.
---
 interp/notation_ops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index e51c691367..448881dcf9 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -509,7 +509,9 @@ let notation_constr_of_glob_constr nenv a =
 
 let notation_constr_of_constr avoiding t =
   let t = EConstr.of_constr t in
-  let t = Detyping.detype Detyping.Now false avoiding (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 avoiding env evd t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
     ninterp_rec_vars = Id.Map.empty;
-- 
cgit v1.2.3