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.

---
 intf/tacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 530213b7cf..493c0939a5 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -209,6 +209,7 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacDo of int or_var * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacTimeout of int or_var * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
+  | TacTime of string option * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacRepeat of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacProgress of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacShowHyps of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
-- 
cgit v1.2.3