X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;fp=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=cf6b6eeffba96fb5796f7049c025a3635730829b;hb=4d765cc85e3a1e84c80c348a1e67ea1eed984916;hp=fa773a4db8450d1705070c6256b6216400fd919c;hpb=6b1cb7a439b2e72ec3d6bbb9803e880c82d85020;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index fa773a4db..cf6b6eeff 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -474,8 +474,14 @@ let add_eq u v b =
 let rank = ref MAL.empty;;
 
 let do_rank (b,_,_) =
-(*         print_ugraph ugraph; *)
-   let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
+   let keys = 
+     MAL.fold 
+       (fun k v acc -> 
+          SOF.union acc (SOF.union (SOF.singleton k) 
+            (SOF.union v.eq_closure (SOF.union v.gt_closure v.ge_closure))))
+       b SOF.empty 
+   in
+   let keys = SOF.elements keys in
    let fall =
      List.fold_left 
        (fun acc u ->
@@ -483,7 +489,6 @@ let do_rank (b,_,_) =
            | [] -> 0, seen
            | x::tl when SOF.mem x seen -> aux k seen tl
            | x::tl ->
-(*                prerr_endline (String.make k '.' ^ string_of_universe x); *)
                let seen = SOF.add x seen in
                let t1, seen = aux (k+1) seen (SOF.elements (repr x b).eq_closure) in
                let t3, seen = aux (k+1) seen (SOF.elements (repr x b).gt_closure) in