X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=fa773a4db8450d1705070c6256b6216400fd919c;hb=ca41435a6021292ccba239aa173651c0be705b45;hp=c8a8660b3bade7c485670c89087291f5a222944d;hpb=680ab4fda3d69308fda744f79a8bf20a79e0a472;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index c8a8660b3..fa773a4db 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -498,9 +498,12 @@ let do_rank (b,_,_) =
        MAL.empty
    in
    rank := fall keys;
+   let res = ref [] in
    MAL.iter 
      (fun k v -> 
-       prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank
+        if not (List.mem v !res) then res := v::!res;
+       prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank;
+   !res 
 ;;
 
 let get_rank u =