Debugging improved.

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 63231324237aaffb44a8386a61e4bfab239a8ed6..c3765f3f0261eb092bbb93e87c8e12df6d0a9bc7 100644 (file)
--- 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: *)