From df96068caabe1a3fd9ff301fe24b2b1d20d8f2aa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 Nov 2013 15:51:17 -0800
Subject: [PATCH] fix(library/tactic): clean up try_for

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/tactic.cpp | 4 ++--
 src/library/tactic/tactic.h   | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 39b89077a8..ee2d74a69e 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -131,13 +131,13 @@ tactic try_for(tactic t, unsigned ms, unsigned check_ms) {
             try {
                 auto start = std::chrono::steady_clock::now();
                 std::chrono::milliseconds d(ms);
-                std::chrono::milliseconds one(1);
+                std::chrono::milliseconds small(check_ms);
                 while (!done) {
                     auto curr = std::chrono::steady_clock::now();
                     if (std::chrono::duration_cast<std::chrono::milliseconds>(curr - start) > d)
                         break;
                     check_interrupted();
-                    std::this_thread::sleep_for(one);
+                    std::this_thread::sleep_for(small);
                 }
                 th.request_interrupt();
                 th.join();
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index cebd747137..35b9e69c04 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include <utility>
 #include <memory>
 #include <mutex>
-#include "util/interrupt.h"
 #include "util/lazy_list.h"
 #include "library/io_state.h"
 #include "library/tactic/proof_state.h"
@@ -63,6 +62,6 @@ tactic now_tactic();
 tactic assumption_tactic();
 tactic then(tactic t1, tactic t2);
 tactic orelse(tactic t1, tactic t2);
-tactic try_for(tactic t, unsigned ms, unsigned check_ms = g_small_sleep);
+tactic try_for(tactic t, unsigned ms, unsigned check_ms = 1);
 tactic repeat(tactic t1);
 }