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. --- engine/uState.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/uState.ml') diff --git a/engine/uState.ml b/engine/uState.ml index ffb54d441..839bb5ae9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -471,7 +471,7 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level () in + let u = UnivGen.new_univ_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with @@ -582,7 +582,7 @@ let fix_undefined_variables uctx = uctx_univ_algebraic = algs' } let refresh_undefined_univ_variables uctx = - let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in let subst_fn u = Univ.subst_univs_level_level subst u in let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc) uctx.uctx_univ_algebraic Univ.LSet.empty -- cgit v1.2.3