diff options
| author | Matthieu Sozeau | 2020-04-06 14:42:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-04-06 14:42:12 +0200 |
| commit | 2089207415565e8a28816f53b61d9292d04f4c59 (patch) | |
| tree | 9d8edb9e90c93b767ef471ee76e1503624baa878 /test-suite | |
| parent | 28c031158cee24faf782a7192032e29229aee4d4 (diff) | |
| parent | 5a961410854f01a4445b6605483d0b227279a1fd (diff) | |
Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_state
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
Diffstat (limited to 'test-suite')
| -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. |