ranking reports the lest of univs

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index c8a8660b3bade7c485670c89087291f5a222944d..fa773a4db8450d1705070c6256b6216400fd919c 100644 (file)
--- 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 = 

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index 6451a74ec619abf63c65bbc4a6a0c1efe16739ec..b53e506914552d50f949cecd38364823d3a4b2b8 100644 (file)
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -72,7 +72,7 @@ val add_ge:
 val add_gt: 
   universe -> universe -> universe_graph -> universe_graph
 
-val do_rank: universe_graph -> unit
+val do_rank: universe_graph -> int list
 val get_rank: universe -> int
 
 (*