From 5c8876da5e25512842f2acd7cfa8c62200b9a623 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 16:18:11 +0200
Subject: Univs: fix evar_map initialization in newring.

---
 plugins/setoid_ring/newring.ml4 | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index e590958ccf..1c4ba88237 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -155,14 +155,19 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 (****************************************************************************)
 
 let ic c =
-  let env = Global.env() and sigma = Evd.empty in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
   Constrintern.interp_open_constr env sigma c
 
 let ic_unsafe c = (*FIXME remove *)
-  let env = Global.env() and sigma = Evd.empty in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
     fst (Constrintern.interp_constr env sigma c)
 
-let ty c = Typing.unsafe_type_of (Global.env()) Evd.empty c
+let ty c =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+    Typing.unsafe_type_of env sigma c
 
 let decl_constant na ctx c =
   let vars = Universes.universes_of_constr c in
-- 
cgit v1.2.3