]> matita.cs.unibo.it Git - helm.git/commitdiff
ranking reports the lest of univs
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 16 May 2008 17:07:06 +0000 (17:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 16 May 2008 17:07:06 +0000 (17:07 +0000)
helm/software/components/cic/cicUniv.ml
helm/software/components/cic/cicUniv.mli

index c8a8660b3bade7c485670c89087291f5a222944d..fa773a4db8450d1705070c6256b6216400fd919c 100644 (file)
@@ -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 = 
index 6451a74ec619abf63c65bbc4a6a0c1efe16739ec..b53e506914552d50f949cecd38364823d3a4b2b8 100644 (file)
@@ -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
 
 (*