From 05dff3bdaaf474e67b0878bc2dd0952427ce277e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 22 Jun 2018 16:09:23 +0200
Subject: universes_of_constr don't include universes of monomorphic constants

Apparently it was not useful. I don't remember what I was thinking
when I added it.
---
 plugins/setoid_ring/newring.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 84b29a0bfb..e4d17f2504 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -148,8 +148,7 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na univs c =
   let open Constr in
-  let env = Global.env () in
-  let vars = Univops.universes_of_constr env c in
+  let vars = Univops.universes_of_constr c in
   let univs = Univops.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
-- 
cgit v1.2.3