Profiling code commented out.

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index cf6a76cdca29835f60dd5a9691b98cfb62c5865f..698175d1b13b1f5545ff369a469092c056816334 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -66,10 +66,12 @@ let indexing_retrieval_time = ref 0.;;
 let apply_subst = CicMetaSubst.apply_subst
 
 
+(* Profiling code
 let apply_subst =
   let profile = CicUtil.profile "apply_subst" in
-  (fun s a -> profile (apply_subst s) a)
+  (fun s a -> profile.profile (apply_subst s) a)
 ;;
+*)
 
 
 (*
@@ -155,7 +157,7 @@ let get_candidates mode tree term =
 
 (* let get_candidates = *)
 (*   let profile = CicUtil.profile "Indexing.get_candidates" in *)
-(*   (fun mode tree term -> profile (get_candidates mode tree) term) *)
+(*   (fun mode tree term -> profile.profile (get_candidates mode tree) term) *)
 (* ;; *)
 
 
@@ -890,7 +892,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
 
 (*   let build_new = *)
 (*     let profile = CicUtil.profile "Indexing.superposition_right.build_new" in *)
-(*     (fun o e -> profile (build_new o) e) *)
+(*     (fun o e -> profile.profile (build_new o) e) *)
 (*   in *)
   
   let new1 = List.map (build_new U.Gt) res1