X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUtil.ml;h=81834251577822662c5121c70ea0cf98a11aaf5f;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=07f39896c3050396c9e72a194c88931cfe3d7158;hpb=938afa2d17a731cef4b7226aa9c1bc7c3b7de2fe;p=helm.git diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 07f39896c..818342515 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -209,28 +209,6 @@ let rec mk_rels howmany from = | 0 -> [] | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from) -let profiling_enabled = false - -type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } -let profile = - if profiling_enabled then - function s -> - let total = ref 0.0 in - let profile f x = - let before = Unix.gettimeofday () in - let res = f x in - let after = Unix.gettimeofday () in - total := !total +. (after -. before); - res - in - at_exit - (fun () -> - print_endline - ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); - { profile = profile } - else - function _ -> { profile = fun f x -> f x } - let id_of_annterm = function | Cic.ARel (id,_,_,_)