| 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,_,_,_)