From 33388d18f0165369a565cd5ca5b6eb153899271e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 19 Apr 2020 18:04:14 -0400
Subject: Fix the `with_strategy` tactic to work with `abstract`

---
 test-suite/success/with_strategy.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index bf639ae6b9..bacea3549f 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -131,7 +131,7 @@ Qed.
 (* test that the strategy tactic does persist through abstract *)
 Opaque id.
 Goal id 0 = 0.
-  Fail Time Timeout 5
+  Time Timeout 5
        with_strategy
        expand [id]
        assert (id (fact 100) = fact 100) by abstract reflexivity.
-- 
cgit v1.2.3