diff options
author | 2013-03-25 09:33:01 +0000 | |
---|---|---|
committer | 2013-03-25 09:33:01 +0000 | |
commit | 52c3aea2d3a9e03c307166ec667bc7ad90ae4fed (patch) | |
tree | d057e534e6cd481efe285db71aa39079d02c8000 /pretyping/nativenorm.ml | |
parent | 8a13513d5214a91f8bd9b7611675c400ee41a9f3 (diff) |
Native compiler: timing info for reification in debug mode.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16357 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/nativenorm.ml')
-rw-r--r-- | pretyping/nativenorm.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 887773311..9a2a8dce7 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -348,5 +348,9 @@ let native_norm env c ty = let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Pp.msg_debug (Pp.str time_info); - nf_val env !Nativelib.rt1 ty + let res = nf_val env !Nativelib.rt1 ty in + let t2 = Sys.time () in + let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in + if !Flags.debug then Pp.msg_debug (Pp.str time_info); + res | _ -> anomaly (Pp.str "Compilation failure") |