From d29b487f7c50fd8332cb1cfc144f70bc7db595d9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 3 Jul 2014 12:43:28 +0200
Subject: Adding a "time" tactical for benchmarking purposes. In case the
 tactic backtracks, print time spent in each of successive calls.

---
 lib/system.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/system.mli')

diff --git a/lib/system.mli b/lib/system.mli
index 2e286a40c9..9cfb1456ff 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -67,3 +67,5 @@ type time
 val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.std_ppcmds
+
+val with_time : bool -> ('a -> 'b) -> 'a -> 'b
-- 
cgit v1.2.3