X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=2bfbc92a32f999553815ee7f7326ebbe2ee5a3d4;hb=2ed731db1107673f11de9b56a376bee41b4cf0be;hp=699af7847a029b05345ef2c49817561ca92a6e59;hpb=9b9f415916ff4842c69f4918064d5dd64031df63;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 699af7847..2bfbc92a3 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -595,26 +595,27 @@ let add_eq ?fast u v b =
 (* ugly *)
 let rank = ref MAL.empty;;
 
-let do_rank (b,_,_) =
-  
+let do_rank (b,_,_ as ugraph) =
+(*         print_ugraph ugraph; *)
    let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
    let fall =
      List.fold_left 
        (fun acc u ->
-         let rec aux seen = function
+         let rec aux k seen = function
            | [] -> 0, seen
-           | x::tl when SOF.mem x seen -> aux seen tl
+           | 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 seen (SOF.elements (repr x b).one_s_eq) in
-               let t2, seen = aux seen (SOF.elements (repr x b).one_s_ge) in
-               let t3, seen = aux seen (SOF.elements (repr x b).one_s_gt) in
-               let t4, seen = aux seen tl 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
+               let t2, seen = aux (k+1) seen (SOF.elements (repr x b).ge_closure) in
+               let t4, seen = aux k seen tl in
                max (max t1 t2) 
-                 (max (if SOF.is_empty (repr x b).one_s_gt then 0 else t3+1) t4),
+                 (max (if SOF.is_empty (repr x b).gt_closure then 0 else t3+1) t4),
                seen 
          in
-         let rank, _ = aux SOF.empty [u] in
+         let rank, _ = aux 0 SOF.empty [u] in
          MAL.add u rank acc) 
        MAL.empty
    in