print_endline => prerr_endline

[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index a4bdef1a2a48b0121246ead95c73f21edb56183a..f3af1b482e8afb2eece8d1ce79d3e10af7812ec7 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id$ *)
 
@@ -180,15 +180,9 @@ let get_candidates ?env mode tree term =
   let s = 
     match mode with
     | Matching -> 
-        let _ = <:start<retrieve_generalizations>> in
-        <:stop<retrieve_generalizations
         Index.retrieve_generalizations tree term
-        >>
     | Unification -> 
-        let _ = <:start<retrieve_unifiables>> in
-        <:stop<retrieve_unifiables
         Index.retrieve_unifiables tree term
-        >>
         
   in
   Index.PosEqSet.elements s
@@ -1039,4 +1033,4 @@ let rec demodulation_goal env table goal =
   | None -> do_right ()
 ;;
 
-let get_stats () = <:show<Indexing.>> ;;
+let get_stats () = "" ;;