From: Enrico Tassi Date: Wed, 23 Jul 2008 16:12:36 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~4882 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=f72ad4ff2fd12310fb7915f74721697b928b9aea;p=helm.git ... --- diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index 467d61147..164e1a223 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -142,10 +142,10 @@ let _ = try load_graph u with exn -> ()) roots_alluris; prerr_endline "finished...."; - let lll,uuu = List.sort compare (CicUniv.do_rank (get_graph ())) in + let lll, uuu =(CicUniv.do_rank (get_graph ())) in + let lll = List.sort compare lll in List.iter (fun k -> - prerr_endline (string_of_universe k ^ " = " ^ string_of_int (Cicuniv.get_rank k))) uuu - in + prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int (CicUniv.get_rank k))) uuu; let _ = try let rec aux = function