X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=c3765f3f0261eb092bbb93e87c8e12df6d0a9bc7;hb=6ca18231c6abf1e39bb8129c2369f9c0def64d67;hp=63231324237aaffb44a8386a61e4bfab239a8ed6;hpb=f81e6df71f8804c2f491034b951dcd34e0bd24c3;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 632313242..c3765f3f0 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -24,8 +24,6 @@ let times = ref [];;
 let pp s =
  if !debug then
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
- else 
-  ()
 ;;
 let inside c =
  if !debug then
@@ -860,12 +858,4 @@ let typeof_obj
       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
 ;;
 
-let typeof st ?localise m s c t1 t2 =
-let time1 = Unix.gettimeofday () in
-let res = typeof st ?localise m s c t1 t2 in
-let time2 = Unix.gettimeofday () in
-prerr_endline ("OVERALL TYPEOF TIME: " ^ string_of_float (time2 -. time1));
-res
-;;
-
 (* vim:set foldmethod=marker: *)