From ccae6b2053970a0bd587bb48c2d30fc235de4118 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 7 Jun 2019 10:54:14 +0200
Subject: restrict minimization to set to flexibles

Split from #10331
Fix part of #8196
Replaces #9343
---
 engine/univMinim.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 30fdd28997..fc0770cf75 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -276,7 +276,7 @@ let normalize_context_set ~lbound g ctx us algs weak =
     Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts
   in
   let smallles = if get_set_minimization ()
-    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
+    then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles
     else Constraint.empty
   in
   let csts, partition =
-- 
cgit v1.2.3