Merge PR #14042: Fix a bug in UnivProblem

Reviewed-by: SkySkimmer
Reviewed-by: ppedrot

1 files changed, 1 insertions, 1 deletions

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