diff options
| author | Hugo Herbelin | 2014-07-03 12:43:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-07-13 18:02:57 +0200 |
| commit | d29b487f7c50fd8332cb1cfc144f70bc7db595d9 (patch) | |
| tree | a80671a48c3db293d46f5d8d2a929486a4d02e13 /lib/system.mli | |
| parent | d90205f6284b998a8fc50b295d2d790d2580ea26 (diff) | |
Adding a "time" tactical for benchmarking purposes. In case the tactic
backtracks, print time spent in each of successive calls.
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |