From a3503c0aca07f5e7f5785faa7b76123a02ecc2af Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 7 Jul 2014 21:34:49 +0200
Subject: Revert "time tac" (committed by mistake).

This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
---
 intf/tacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e64dcb62c1..530213b7cf 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -209,7 +209,6 @@ 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