From abad0a15ac44cb5b53b87382bb4d587d9800a0f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 3 Jul 2014 12:43:28 +0200
Subject: time tac

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 530213b7cf..e64dcb62c1 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 ('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