Profiling code for merge_ugraphs commented out (since profiling is much more

expensive than the profiled code).

diff --git a/components/cic/cicUniv.ml b/components/cic/cicUniv.ml
index 8ae118c9b1bb5ecf1d4c656ffcfb2bfb4ba15c86..b7783095414d47d56a38fe65679c8ba322353088 100644 (file)
--- a/components/cic/cicUniv.ml
+++ b/components/cic/cicUniv.ml
@@ -600,10 +600,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                                           **)