diff options
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index dbf5d48aa..844eb390b 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -20,7 +20,7 @@ type uinfo = { uloc : Loc.t option; } -module UPairSet = Universes.UPairSet +module UPairSet = UnivMinim.UPairSet (* 2nd part used to check consistency on the fly. *) type t = @@ -630,7 +630,7 @@ let refresh_undefined_univ_variables uctx = uctx', subst let minimize uctx = - let open Universes in + let open UnivMinim in let ((vars',algs'), us') = normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints |