diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_4544.v')
| -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. |