From db22ae6140259dd065fdd80af4cb3c3bab41c184 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 2 Oct 2018 13:44:46 +0000
Subject: rename test files (do not start by a digit)

---
 test-suite/bugs/closed/2616.v | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100644 test-suite/bugs/closed/2616.v

(limited to 'test-suite/bugs/closed/2616.v')

diff --git a/test-suite/bugs/closed/2616.v b/test-suite/bugs/closed/2616.v
deleted file mode 100644
index 8758e32dd8..0000000000
--- a/test-suite/bugs/closed/2616.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* Testing ill-typed rewrite which used to succeed in 8.3 *)
-Goal 
-  forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0), 
-    N 0 -> False.
-Proof.
-intros.
-Fail rewrite IN in H.
-- 
cgit v1.2.3