From 748a33cee41900d285897b24b4d8e29dd9eb2a3d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 28 Apr 2018 21:36:57 +0200
Subject: Split off Universes functions for minimization.

This finishes the splitting of 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 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
-- 
cgit v1.2.3