]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUniv.ml
restored old (r6662) behaviour
[helm.git] / helm / software / components / cic / cicUniv.ml
index 8ae118c9b1bb5ecf1d4c656ffcfb2bfb4ba15c86..0d75caf898cec408590e0f82a59aaf22bfa4b085 100644 (file)
@@ -554,6 +554,7 @@ let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) =
   end_spending ();
     rc,already_contained
     
+(* profiling code
 let profiler_eq = HExtlib.profile "CicUniv.add_eq"
 let profiler_ge = HExtlib.profile "CicUniv.add_ge"
 let profiler_gt = HExtlib.profile "CicUniv.add_gt"
@@ -563,6 +564,7 @@ let add_ge ?fast u v b =
   profiler_ge.HExtlib.profile (fun _ -> add_ge ?fast u v b) ()
 let add_eq ?fast u v b = 
   profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) ()
+*)
 
 (*****************************************************************************)
 (** END: Decomment this for performance comparisons                         **)
@@ -600,10 +602,13 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) =
     fst (merge_brutal increment base_ugraph), 
     UriManager.UriSet.add uri_of_increment already_contained
 
-let profiler_merge = HExtlib.profile "CicUniv.merge_graphs"
+(* profiling code; WARNING: the time spent during profiling can be
+   greater than the profiled time
+let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs"
 let merge_ugraphs ~base_ugraph ~increment =
   profiler_merge.HExtlib.profile 
   (fun _ -> merge_ugraphs ~base_ugraph ~increment) ()
+*)
 
 (*****************************************************************************)
 (** Xml sesialization and parsing                                           **)