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

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

diff --git a/test-suite/bugs/closed/2393.v b/test-suite/bugs/closed/2393.v
deleted file mode 100644
index fb4f92619f..0000000000
--- a/test-suite/bugs/closed/2393.v
+++ /dev/null
@@ -1,13 +0,0 @@
-Require Import Program.
-
-Inductive T := MkT.
-
-Definition sizeOf (t : T) : nat
-    := match t with
-       | MkT => 1
-       end.
-Variable vect : nat -> Type.
-Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T
-    := match t with
-       | MkT => MkT
-       end.
-- 
cgit v1.2.3