From 5e690404233e6c772c1d5ddc52142edf474953ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 May 2017 21:47:12 +0200
Subject: Cleaning old untested not any more interesting testing files.

---
 test-suite/kernel/inds.mv | 3 ---
 1 file changed, 3 deletions(-)
 delete mode 100644 test-suite/kernel/inds.mv

(limited to 'test-suite/kernel')

diff --git a/test-suite/kernel/inds.mv b/test-suite/kernel/inds.mv
deleted file mode 100644
index bd1cc49f86..0000000000
--- a/test-suite/kernel/inds.mv
+++ /dev/null
@@ -1,3 +0,0 @@
-Inductive [] nat : Set := O : nat | S : nat->nat.
-Check Construct nat 0 1.
-Check Construct nat 0 2.
-- 
cgit v1.2.3