From b1f764f51ba02fdb4d7a7582f410816286a500d6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Jan 2006 15:15:39 +0000 Subject: [PATCH] debug prints commented --- helm/ocaml/library/librarySync.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index abb50f363..92926464b 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -191,7 +191,16 @@ let add_single_obj uri obj ~basedir = if CicEnvironment.in_library uri then raise (AlreadyDefined uri) else begin + (*CicUniv.reset_spent_time (); + let before = Unix.gettimeofday () in*) typecheck_obj uri obj; (* 1 *) + (*let after = Unix.gettimeofday () in + let univ_time = CicUniv.get_spent_time () in + let total_time = after -. before in + prerr_endline + (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" + (univ_time *. 100. /. total_time) (total_time) (univ_time) + (UriManager.name_of_uri uri));*) let _, ugraph, univlist = CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in try -- 2.39.2