From 6ca18231c6abf1e39bb8129c2369f9c0def64d67 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 Oct 2009 21:03:49 +0000 Subject: [PATCH] Debugging improved. --- helm/software/components/ng_refiner/nCicRefiner.ml | 10 ---------- 1 file changed, 10 deletions(-) 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: *) -- 2.39.2