From 5b8b02cd060097c3c980b0498257c30eda1ad207 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 5 Dec 2017 20:22:14 +0100
Subject: Fix #6323: stronger restrict universe context vs abstract.

In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.

Universes of a monomorphic reference [c] are considered to appear in
the term [c].
---
 plugins/setoid_ring/newring.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index f22f00839a..e3e749b754 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -152,7 +152,8 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na univs c =
   let open Constr in
-  let vars = Univops.universes_of_constr c in
+  let env = Global.env () in
+  let vars = Univops.universes_of_constr env 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