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

---
 engine/evarutil.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'engine/evarutil.ml')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 2b6913c0b7..fdb14b7251 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -815,8 +815,7 @@ let subterm_source evk (loc,k) =
 
 let try_soft evd u u' =
   let open Universes in
-  let make = Univ.Universe.make in
-  try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u'))
+  try Evd.add_universe_constraints evd (Constraints.singleton (ULub (u, u')))
   with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd
 
 (* Add equality constraints for covariant/invariant positions. For
-- 
cgit v1.2.3