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/opened/2447.v | 6 ------
 1 file changed, 6 deletions(-)
 delete mode 100644 test-suite/bugs/opened/2447.v

(limited to 'test-suite/bugs/opened')

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