From 676c93e4bee82a4e6528fbf42be28efe473b1871 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Tue, 19 Jun 2018 19:03:52 +0200
Subject: Fix Univ.enforce_leq dropped constraints when algebraic on the right

There's probably a proof of false using subtyping if someone wants to
look.

NB: the checker doesn't handle algebraics on the right.
---
 kernel/univ.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9782312ca..2b4a1c50c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -674,12 +674,7 @@ let check_univ_leq u v =
   Universe.for_all (fun u -> check_univ_leq_one u v) u
 
 let enforce_leq u v c =
-  let rec aux acc v =
-  match v with
-  | v :: l ->
-    aux (List.fold_right (fun u -> constraint_add_leq u v) u c) l
-  | [] -> acc
-  in aux c v
+  List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
-- 
cgit v1.2.3