From 65f0b34c9740788270b48700a7ce2b5338ba1f64 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Apr 2021 01:33:33 +0200
Subject: Fix a bug in UnivProblem

---
 engine/univProblem.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/univProblem.ml')

diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 8d6689933c..7ac6ca1180 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -30,7 +30,7 @@ let subst_univs fn = function
   | UEq (u, v) ->
     let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
     if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
+    else Some (UEq (u',v'))
   | ULub (u, v) ->
     let u' = level_subst_of fn u and v' = level_subst_of fn v in
     if Level.equal u' v' then None
-- 
cgit v1.2.3