From d236c7362053c4fc8f1c7f3b59248b412b029fb8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 21 Jun 2018 18:02:40 +0200
Subject: Define and use UGraph.enforce_leq_alg for subtyping inference

Not sure if worth using in other places.
---
 kernel/reduction.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f4af313867..2c61b7a019 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -693,8 +693,8 @@ let infer_eq (univs, cstrs as cuniv) u u' =
 let infer_leq (univs, cstrs as cuniv) u u' =
   if UGraph.check_leq univs u u' then cuniv
   else
-    let cstrs' = Univ.enforce_leq u u' cstrs in
-      univs, cstrs'
+    let cstrs', _ = UGraph.enforce_leq_alg u u' univs in
+      univs, Univ.Constraint.union cstrs cstrs'
 
 let infer_cmp_universes env pb s0 s1 univs =
   let open Sorts in
-- 
cgit v1.2.3