X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;fp=helm%2Fmatita%2FmatitaSync.ml;h=5dc3e2d248743311a92a2a7a584b6110833b11ba;hb=f2cda8d3c554ceafb87198ea4cd223242fe67c94;hp=84d107f30d599596549627b94b19ae2075bda9d6;hpb=9826bf0a143ca0563cb4b29a6bdfe1df7efd2a04;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 84d107f30..5dc3e2d24 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -110,6 +110,11 @@ let paths_and_uris_of_obj uri status =
   let xmlbodypath = basedir ^ "/" ^  xmlbodyfilename in
   xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri
 
+let acic_object_of_cic_object =
+ let profiler = CicUtil.profile "add_obj.save_object_to_disk.acic_object_of_cic_object" in
+  fun ~eta_fix obj ->
+   profiler.CicUtil.profile (Cic2acic.acic_object_of_cic_object ~eta_fix) obj
+
 let save_object_to_disk status uri obj =
   let ensure_path_exists path =
     let dir = Filename.dirname path in
@@ -117,7 +122,7 @@ let save_object_to_disk status uri obj =
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
-    Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
+    acic_object_of_cic_object ~eta_fix:false obj
   in 
   (* prepare XML *)
   let xml, bodyxml =