diff options
| author | Jason Gross | 2020-04-19 18:04:14 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 13:03:04 -0400 |
| commit | 33388d18f0165369a565cd5ca5b6eb153899271e (patch) | |
| tree | c706101cca1c78cae71b017e2127ad2068eab547 /test-suite | |
| parent | 2edbbfee7fdcfb2a4804524091930c5dab7b9db4 (diff) | |
Fix the `with_strategy` tactic to work with `abstract`
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/with_strategy.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |