time tac

1 files changed, 13 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index c478bd6635..da1937ef3d 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -579,6 +579,19 @@ let tclTIMEOUT n t =
         Proof.ret res
     | Util.Inr e -> tclZERO e
 
+let tclTIME t =
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  let t = Proof.lift (Proofview_monad.NonLogical.ret ()) >> t in
+  Proof.current >>= fun env ->
+  Proof.get >>= fun initial ->
+  Proof.lift begin
+    Proofview_monad.NonLogical.time !Flags.time (Proof.run t env initial)
+  end >>= function ((res,s),m) ->
+    Proof.set s >>
+    Proof.put m >>
+    Proof.ret res
+
 let mark_as_unsafe =
   Proof.put (false,([],[]))