]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUtil.ml
CicUtil.profile made even more polymorphic.
[helm.git] / helm / ocaml / cic / cicUtil.ml
index aa1ed1ba0ec745e30d169dba355703127e7c9629..c85c2c803719f58ea3ec0ea6349c9bf0043c2566 100644 (file)
@@ -209,8 +209,9 @@ let rec mk_rels howmany from =
   | 0 -> []
   | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
 
-let profiling_enabled = false
+let profiling_enabled = true
 
+type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
 let profile =
  if profiling_enabled then
   function s ->
@@ -226,9 +227,9 @@ let profile =
     (fun () ->
       print_endline
        ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total));
-   profile
+   { profile = profile }
  else
-  function _ -> fun f x -> f x
+  function _ -> { profile = fun f x -> f x }
 
 let id_of_annterm =
   function