From fcabdf5805add91a036fe5d11c7f47cfcec91d56 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Sep 2005 09:05:53 +0000
Subject: [PATCH] Profiling code commented out.

---
 helm/ocaml/paramodulation/indexing.ml |  8 +++++---
 helm/ocaml/tactics/autoTactic.ml      |  4 +++-
 helm/ocaml/tactics/metadataQuery.ml   | 14 +++++++++-----
 3 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index cf6a76cdc..698175d1b 100644
--- 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
diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 85c5c54be..38a5d59d3 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -27,10 +27,12 @@
 
 (* let debug_print = fun _ -> () *)
 
+(* Profiling code
 let new_experimental_hint =
  let profile = CicUtil.profile "new_experimental_hint" in
  fun ~dbd ~facts ?signature ~universe status ->
-  profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status
+  profile.profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status
+*) let new_experimental_hint = MetadataQuery.new_experimental_hint
 
 (* In this versions of auto_tac we maintain an hash table of all inspected
    goals. We assume that the context is invariant for application. 
diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 9f0cff9ad..e86f79af5 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -123,14 +123,16 @@ let intersect uris siguris =
   let inter = Constr.UriManagerSet.inter set1 set2 in
   List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
 
+(* Profiling code
 let at_most =
  let profiler = CicUtil.profile "at_most" in
- fun ~dbd ~where uri -> profiler (Constr.at_most ~dbd ~where) uri
+ fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
 
 let sigmatch =
  let profiler = CicUtil.profile "sigmatch" in
  fun ~dbd ~facts ~where signature ->
-  profiler (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
+  profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
+*) let at_most = Constr.at_most  let sigmatch = MetadataConstraints.sigmatch
 
 let filter_uris_forward ~dbd (main, constants) uris =
   let main_uris =
@@ -219,17 +221,19 @@ let close_with_constructors s metasenv context =
 	| _ -> bag)
     s s
 
+(* Profiling code
 let apply_tac_verbose =
  let profiler = CicUtil.profile "apply_tac_verbose" in
-  fun ~term status -> profiler (PrimitiveTactics.apply_tac_verbose ~term) status
+  fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
 
 let sigmatch =
  let profiler = CicUtil.profile "sigmatch" in
- fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler (Constr.sigmatch ~dbd ~facts ~where) signature
+ fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
 
 let cmatch' =
  let profiler = CicUtil.profile "cmatch'" in
- fun ~dbd ~facts signature -> profiler (Constr.cmatch' ~dbd ~facts) signature
+ fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
+*) let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch'
 
 let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
  let (_, metasenv, _, _) = proof in
-- 
2.39.2