From 811df9475898045b720f804c7d49638faa4e8478 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 16 Dec 2014 16:55:43 +0100
Subject: Moving #2447 (congruence) to fixed.

---
 test-suite/bugs/closed/2447.v | 7 +++++++
 test-suite/bugs/opened/2447.v | 6 ------
 2 files changed, 7 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/bugs/closed/2447.v
 delete mode 100644 test-suite/bugs/opened/2447.v

diff --git a/test-suite/bugs/closed/2447.v b/test-suite/bugs/closed/2447.v
new file mode 100644
index 0000000000..fdeb69fcc7
--- /dev/null
+++ b/test-suite/bugs/closed/2447.v
@@ -0,0 +1,7 @@
+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.
+Proof.
+intros; congruence. (* was doing stack overflow *)
+Qed.
diff --git a/test-suite/bugs/opened/2447.v b/test-suite/bugs/opened/2447.v
deleted file mode 100644
index 503a85d41c..0000000000
--- a/test-suite/bugs/opened/2447.v
+++ /dev/null
@@ -1,6 +0,0 @@
-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.
-Proof.
-Timeout 5 (intros; congruence).
-- 
cgit v1.2.3