aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--proofs/proofview.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6074a13d4..8df23a8bd 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -606,6 +606,7 @@ let tclTIME s t =
msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++
System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in
let rec aux n t =
+ tclUNIT () >>= fun () ->
let tstart = System.get_time() in
Proof.split t >>= function
| Nil e ->