X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=f3af1b482e8afb2eece8d1ce79d3e10af7812ec7;hb=7b4d519aefac94afb371a7e4da94779b40bf8608;hp=a4bdef1a2a48b0121246ead95c73f21edb56183a;hpb=b0bbbe6ec20a0afa145c1e6d92530105d9d4d7e3;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index a4bdef1a2..f3af1b482 100644
--- 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 () = "" ;;