From d640b676282285d52ac19038d693080e64eb5ea7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 1 Mar 2018 15:19:52 +0100
Subject: Statically enforce that ULub is only between levels.

---
 engine/universes.mli | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'engine/universes.mli')

diff --git a/engine/universes.mli b/engine/universes.mli
index a86b9779b..4af944347 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -71,12 +71,16 @@ val new_sort_in_family : Sorts.family -> Sorts.t
     not be necessary if unfolding is performed.
 *)
 
-type universe_constraint_type = ULe | UEq | ULub
+type universe_constraint =
+  | ULe of Universe.t * Universe.t
+  | UEq of Universe.t * Universe.t
+  | ULub of Level.t * Level.t
 
-type universe_constraint = Universe.t * universe_constraint_type * Universe.t
 module Constraints : sig
   include Set.S with type elt = universe_constraint
 
+  val is_trivial : universe_constraint -> bool
+
   val pr : t -> Pp.t
 end
 
-- 
cgit v1.2.3