From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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.
---
 dev/base_include | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 2f5d8aa84..8d81ca3e0 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -204,7 +204,9 @@ let e s =
    implicit syntax *)
 
 let constr_of_string s = 
-  Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);;
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Constrintern.interp_constr env sigma (parse_constr s);;
 
 (* get the body of a constant *)
 
-- 
cgit v1.2.3