]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUtil.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic / cicUtil.ml
index 8bb137f204ae241bc06b5585dc84a61de8ae5a04..81834251577822662c5121c70ea0cf98a11aaf5f 100644 (file)
@@ -209,34 +209,6 @@ let rec mk_rels howmany from =
   | 0 -> []
   | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
 
-let profiling_enabled = true
-
-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
-    try
-     let res = f x in
-     let after = Unix.gettimeofday () in
-      total := !total +. (after -. before);
-      res
-    with
-     exc ->
-      let after = Unix.gettimeofday () in
-       total := !total +. (after -. before);
-       raise exc
-   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,_,_,_)