From db8e0d7ecaf233ae73705d2f57635a38f8825dad Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 Oct 2014 19:10:07 +0200
Subject: Adding a timeout to bug #2447.

---
 test-suite/bugs/opened/2447.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/test-suite/bugs/opened/2447.v b/test-suite/bugs/opened/2447.v
index eeb38386b2..503a85d41c 100644
--- a/test-suite/bugs/opened/2447.v
+++ b/test-suite/bugs/opened/2447.v
@@ -2,4 +2,5 @@ Record t := {x : bool; y : bool; z : bool}.
 
 Goal forall x1 x2 y z,
   {| x := x1; y := y; z := z |} = {| x := x2; y := y; z := z |} -> x1 = x2.
-intros; congruence.
+Proof.
+Timeout 5 (intros; congruence).
-- 
cgit v1.2.3