X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=3074f2a78778143141bcb79dd516df2f69af1110;hb=c14ddc094a1cfa93b5337e5aecc6831f72dfc22b;hp=cf6b6eeffba96fb5796f7049c025a3635730829b;hpb=4d765cc85e3a1e84c80c348a1e67ea1eed984916;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index cf6b6eeff..3074f2a78 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -357,6 +357,8 @@ type universe_graph = bag * UriManager.UriSet.t * bool
 
 let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
 let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
+(* FG: default choice for a ugraph ??? *)
+let default_ugraph = oblivion_ugraph   
 
 let current_index_anon = ref (-1)
 let current_index_named = ref (-1)
@@ -504,11 +506,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 =