diff options
| author | Pierre-Marie Pédrot | 2020-03-29 15:29:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-03 19:32:13 +0200 |
| commit | 5a961410854f01a4445b6605483d0b227279a1fd (patch) | |
| tree | 237d3096f221dfb932f89bcaba5b32ca62abd0ec | |
| parent | b5f2b861a3d391716e976469a1a100536550bef8 (diff) | |
Fix the test for bug #4544.
It seems that this PR is making the rewrite much, much faster.
| -rw-r--r-- | test-suite/bugs/closed/bug_4544.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_4544.v b/test-suite/bugs/closed/bug_4544.v index 13c47edc8f..e9e9c552f6 100644 --- a/test-suite/bugs/closed/bug_4544.v +++ b/test-suite/bugs/closed/bug_4544.v @@ -1003,7 +1003,8 @@ Proof. = loops_functor (group_loops_functor (pmap_compose psi phi)) g). rewrite <- p. - Fail Timeout 1 Time rewrite !loops_functor_group. + Timeout 1 Time rewrite !loops_functor_group. + Undo. (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *) Timeout 1 do 3 rewrite loops_functor_group. Abort. |