From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Oct 2009 21:03:49 +0000 (+0000)
Subject: Debugging improved.
X-Git-Tag: make_still_working~3294
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6ca18231c6abf1e39bb8129c2369f9c0def64d67;p=helm.git

Debugging improved.
---

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: *)