time tac

3 files changed, 17 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,([],[]))
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6a2d815114..df833a04ff 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -261,6 +261,9 @@ exception Timeout
     In case of timeout if fails with [tclZERO Timeout]. *)
 val tclTIMEOUT : int -> 'a tactic -> 'a tactic
 
+(** [tclTIME t] displays time for each atomic call to t *)
+val tclTIME : 'a tactic -> 'a tactic
+
 (** [mark_as_unsafe] signals that the current tactic is unsafe. *)
 val mark_as_unsafe : unit tactic
 
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 4d4e4470c0..8139d3026b 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -38,6 +38,7 @@ module NonLogical : sig
   val raise : exn -> 'a t
   val catch : 'a t -> (exn -> 'a t) -> 'a t
   val timeout : int -> 'a t -> 'a t
+  val time : bool -> 'a t -> 'a t
 
 
   (* [run] performs effects. *)