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.
---
 pretyping/patternops.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 375ed10d0d..9342b4cc76 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -279,9 +279,11 @@ let lift_pattern k = liftn_pattern k 1
 let rec subst_pattern subst pat =
   match pat with
   | PRef ref ->
-      let ref',t = subst_global subst ref in
-	if ref' == ref then pat else
-	 pattern_of_constr (Global.env()) Evd.empty t
+    let ref',t = subst_global subst ref in
+    if ref' == ref then pat else
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      pattern_of_constr env evd t
   | PVar _
   | PEvar _
   | PRel _ -> pat
-- 
cgit v1.2.3