diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 21:36:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:47:10 +0200 |
| commit | 748a33cee41900d285897b24b4d8e29dd9eb2a3d (patch) | |
| tree | 1cac3f0d220fecc75e5b445f8b65d8d224d76c77 /engine/uState.ml | |
| parent | d41eaff0b2c6f2ff10ef851864abfa3366862d22 (diff) | |
Split off Universes functions for minimization.
This finishes the splitting of Universes.
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 |