From 76c3b40482978fffca50f6f59e8bcae455680aba Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 May 2015 16:15:11 +0200
Subject: #3953 now closed.

---
 test-suite/bugs/opened/3953.v | 4 ----
 1 file changed, 4 deletions(-)
 delete mode 100644 test-suite/bugs/opened/3953.v

diff --git a/test-suite/bugs/opened/3953.v b/test-suite/bugs/opened/3953.v
deleted file mode 100644
index d90ae31e8f..0000000000
--- a/test-suite/bugs/opened/3953.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Goal forall (a b : unit), a = b -> exists c, b = c.
-intros.
-eexists.
-Fail subst.
-- 
cgit v1.2.3