From a51dda2344679dc6d9145f3f34acad29721f6c75 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 28 Apr 2018 19:26:21 +0200
Subject: Split off Universes functions dealing with generating new universes.

---
 plugins/nsatz/nsatz.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 81b44ffad..d2d4639d2 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -136,7 +136,7 @@ let mul = function
   | (Const n,q) when eq_num n num_1 -> q
   | (p,q) -> Mul(p,q)
 
-let gen_constant msg path s = Universes.constr_of_global @@
+let gen_constant msg path s = UnivGen.constr_of_global @@
   coq_reference msg path s
 
 let tpexpr  = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
-- 
cgit v1.2.3