From aa5e962c9888889380ae85a7cbd82a8ac4779a0f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 28 Apr 2018 17:26:18 +0200
Subject: Make set minimization option internal to Universes

---
 engine/universes.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'engine/universes.mli')

diff --git a/engine/universes.mli b/engine/universes.mli
index df2e961d6..46d65f257 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -17,9 +17,6 @@ open Univ
 (** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
 module UPairSet : CSet.S with type elt = (Level.t * Level.t)
 
-val set_minimization : bool ref
-val is_set_minimization : unit -> bool
-
 (** Universes *)
 
 val pr_with_global_universes : Level.t -> Pp.t
-- 
cgit v1.2.3