From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 23 Apr 2008 08:17:26 +0000 (+0000)
Subject: Avoid other comparisons on universes using =.
X-Git-Tag: make_still_working~5293
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e2d3b0cabf805137a08f969840da05f8aba0adb;p=helm.git

Avoid other comparisons on universes using =.
---

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 25f70bc0f..8570c0c15 100644
--- 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 =