From 832269bdc098f021af72619c5f5c7547c0121770 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 May 2008 17:07:06 +0000 Subject: [PATCH] ranking reports the lest of univs --- helm/software/components/cic/cicUniv.ml | 5 ++++- helm/software/components/cic/cicUniv.mli | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) 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 = diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli index 6451a74ec..b53e50691 100644 --- 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 (* -- 2.39.2