CicUtil.profile ==> HExtlib.profile

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index cd4d42420de20f6ddc815d7bbbaa80a60f43955f..22819536fe31b02ea993b8cf3dcc6185c549b5d2 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -135,10 +135,10 @@ type disambiguator_thing =
  }
 
 let disambiguate_thing =
- let profiler = CicUtil.profile "disambiguate_thing" in
+ let profiler = HExtlib.profile "disambiguate_thing" in
   { do_it =
      fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
-     -> profiler.CicUtil.profile
+     -> profiler.HExtlib.profile
          (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
            ~drop_aliases_and_clear_diff) thing
   }

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 79c6a4ddef6ca09fe64b7118009312724f269514..9a194b5ba19e00e3a382b02b0b77fc815eeb2e7d 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -696,7 +696,7 @@ let make_absolute paths path =
    with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
 ;;
        
-let profiler_include = CicUtil.profile "include"
+let profiler_include = HExtlib.profile "include"
 
 let eval_command opts status cmd =
   let status,cmd = disambiguate_command status cmd in
@@ -716,7 +716,7 @@ let eval_command opts status cmd =
         raise (IncludedFileNotCompiled moopath) in
      let stream = Ulexing.from_utf8_channel ic in
      let status = ref status in
-      profiler_include.CicUtil.profile
+      profiler_include.HExtlib.profile
        (!eval_from_stream_ref status stream) (fun _ _ -> ());
       close_in ic;
       !status

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 95dab03607493fb3f56e8ddccecaadefb92cf755..9a8cb10eee436997df984b100a3326befde2c65b 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -43,8 +43,8 @@ let alias_diff ~from status =
     status.aliases []
 
 let alias_diff =
- let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in
- fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status
+ let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
 
 let set_proof_aliases status new_aliases =
  let aliases =
@@ -158,18 +158,13 @@ let save_object_to_disk status uri obj ugraph univlist =
      | _-> assert false) 
 
 let typecheck_obj =
- let profiler = CicUtil.profile "add_obj.typecheck_obj" in
-  fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) obj
+ let profiler = HExtlib.profile "add_obj.typecheck_obj" in
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 
 let index_obj =
- let profiler = CicUtil.profile "add_obj.index_obj" in
+ let profiler = HExtlib.profile "add_obj.index_obj" in
   fun ~dbd ~uri ->
-   profiler.CicUtil.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
-
-let save_object_to_disk =
- let profiler = CicUtil.profile "add_obj.save_object_to_disk" in
-  fun status uri obj ugraph univlist ->
-   profiler.CicUtil.profile (save_object_to_disk status uri obj ugraph) univlist
+   profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 
 let add_obj uri obj status =
   let dbd = MatitaDb.instance () in
@@ -201,8 +196,8 @@ let add_obj uri obj status =
   end
 
 let add_obj =
- let profiler = CicUtil.profile "add_obj" in
-  fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status
+ let profiler = HExtlib.profile "add_obj" in
+  fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
    
 module OrderedUri =
 struct