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

---
 plugins/fourier/fourierR.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 0ea70c19f8..96be1d8934 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -283,15 +283,15 @@ let fourier_lineq lineq1 =
 let get = Lazy.force
 let cget = get
 let eget c = EConstr.of_constr (Lazy.force c)
-let constant path s = Universes.constr_of_global @@
+let constant path s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "Fourier" path s
 
 (* Standard library *)
 open Coqlib
 let coq_sym_eqT = lazy (build_coq_eq_sym ())
-let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ())
-let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ())
-let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ())
+let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ())
+let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ())
+let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ())
 
 (* Rdefinitions *)
 let constant_real = constant ["Reals";"Rdefinitions"]
-- 
cgit v1.2.3