X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Flibrary%2FlibrarySync.ml;h=92926464ba294eeb82d26c6a3f1e0620e9e3016d;hb=be5869cd0bbe16c8a67827723c97d2d4fce4c0bc;hp=abb50f36351b3ca4c641d1440105d40f5732821b;hpb=efec9dde0ebb9ea6b8d8556b92bc0173dcab2cb7;p=helm.git

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