aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/setoid_ring/newring.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 84b29a0bf..e4d17f250 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)