From abad0a15ac44cb5b53b87382bb4d587d9800a0f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 3 Jul 2014 12:43:28 +0200
Subject: time tac

---
 proofs/proofview.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'proofs/proofview.ml')

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,([],[]))
 
-- 
cgit v1.2.3