From 5a961410854f01a4445b6605483d0b227279a1fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 29 Mar 2020 15:29:50 +0200
Subject: Fix the test for bug #4544.

It seems that this PR is making the rewrite much, much faster.
---
 test-suite/bugs/closed/bug_4544.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3