From 44ecd58e9ab5fb0f2c45e9eec76440f84995825c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:20:51 +0200
Subject: {Univops -> Vars}.universes_of_constr

It's basically an occur check so it makes sense to put it in vars
---
 plugins/setoid_ring/newring.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 85e759d152..cf959bd11f 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module CVars = Vars
 open Ltac_plugin
 open Pp
 open Util
@@ -150,7 +151,7 @@ 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 vars = CVars.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


From 6aa0aa37e19457a8c0c3ad36f7bbead058442344 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:41:31 +0200
Subject: {Univops->UState}.restrict_universe_context

Thus the adhoc univops can be removed at the end of the deprecation period.

Should we keep exposing restrict_universe_context or make people go
through restrict?

restrict_universe_context is used directly only by newring, where it's
a choice between

    let univs = UState.restrict_universe_context univs vars in

and

    let univs = UState.(context_set (restrict (of_context_set univs) vars)) in
---
 plugins/setoid_ring/newring.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index cf959bd11f..9585826109 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -152,7 +152,7 @@ let ic_unsafe c = (*FIXME remove *)
 let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
-  let univs = Univops.restrict_universe_context univs vars in
+  let univs = UState.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~univs c),
-- 
cgit v1.2.3