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.

1 files changed, 2 insertions, 2 deletions

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;