From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Oct 2015 19:09:10 +0200
Subject: Splitting kernel universe code in two modules.

1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
---
 kernel/pre_env.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/pre_env.ml')

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 5f3f559a2c..615b9d49ba 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -45,7 +45,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 
 type stratification = {
-  env_universes : universes;
+  env_universes : UGraph.t;
   env_engagement : engagement
 }
 
@@ -93,7 +93,7 @@ let empty_env = {
   env_rel_val = [];
   env_nb_rel = 0;
   env_stratification = {
-    env_universes = initial_universes;
+    env_universes = UGraph.initial_universes;
     env_engagement = (PredicativeSet,StratifiedType) };
   env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
-- 
cgit v1.2.3