Avoid other comparisons on universes using =.

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 25f70bc0f82412b637f03508e7d07b25d9bdf17a..8570c0c15c28f4a11f7818fca9d78a0076251538 100644 (file)
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -648,11 +648,11 @@ let rec clean_ugraph m already_contained f =
   let e_l = 
     MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
       begin
-      k::l end else l) m'' []
+      SOF.add k l end else l) m'' SOF.empty
   in
-    if e_l != [] then
+    if not (SOF.is_empty e_l) then
       clean_ugraph 
-        m'' already_contained (fun u -> (f u) && not (List.mem u e_l))
+        m'' already_contained (fun u -> (f u) && not (SOF.mem u e_l))
     else
       MAL.fold 
         (fun k v x -> if v <> empty_entry then MAL.add k v x else x) 
@@ -661,7 +661,8 @@ let rec clean_ugraph m already_contained f =
 
 let clean_ugraph (m,a,o) l =
   assert(not o);
-  let m, a = clean_ugraph m a (fun u -> List.mem u l) in
+  let l = List.fold_right SOF.add l SOF.empty in
+  let m, a = clean_ugraph m a (fun u -> SOF.mem u l) in
   m, a, o
 
 let assigner_of =