aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/pre_env.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/pre_env.ml')
-rw-r--r--kernel/pre_env.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 5f3f559a2..615b9d49b 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;