CicUtil.profile made even more polymorphic.

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index aa1ed1ba0ec745e30d169dba355703127e7c9629..c85c2c803719f58ea3ec0ea6349c9bf0043c2566 100644 (file)
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -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

diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index cad3abbee9546e093ccfee1cfdb512127c762377..744ac3211925a2f3a81d02ffc774ef0b94539838 100644 (file)
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -64,4 +64,5 @@ val mk_rels : int -> int -> Cic.term list
 (** profile s
  * returns a profiling function; [s] is used for labelling the total time at
    the end of the execution *)
-val profile : string -> ('a -> 'b) -> 'a -> 'b
+type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
+val profile : string -> profiler