]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUniv.ml
better ranking interface
[helm.git] / helm / software / components / cic / cicUniv.ml
index cf6b6eeffba96fb5796f7049c025a3635730829b..03088410f59e3804a3ad527581fb8baef8f19751 100644 (file)
@@ -504,11 +504,12 @@ let do_rank (b,_,_) =
    in
    rank := fall keys;
    let res = ref [] in
+   let resk = ref [] in
    MAL.iter 
      (fun k v -> 
-        if not (List.mem v !res) then res := v::!res;
-       prerr_endline (string_of_universe k ^ " = " ^ string_of_int v)) !rank;
-   !res 
+       if not (List.mem v !res) then res := v::!res;
+       resk := k :: !resk) !rank;
+   !res, !resk
 ;;
 
 let get_rank u =