X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=f3af1b482e8afb2eece8d1ce79d3e10af7812ec7;hb=25871137d6571c7634c967c3b2fc87eab75b9704;hp=a4bdef1a2a48b0121246ead95c73f21edb56183a;hpb=b1c222ae8d9bee83d6c5723533a1395d7353893a;p=helm.git

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