aboutsummaryrefslogtreecommitdiff
path: root/test-suite/kernel
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-17 10:02:19 +0200
committerMaxime Dénès2017-05-17 10:02:19 +0200
commite09a8cf6a2db97b75796a54296683fe12977d018 (patch)
tree02472221f83e6ce9efb42d4c40c36d5f731edcde /test-suite/kernel
parent4b53985c2888827fe030294f95b5975d5e34e4c7 (diff)
parent98a927aefb6df05a957d94cf2fd22d88e9e6c6b6 (diff)
Merge PR#620: Reorganization of the layout for miscellaneous tests
Diffstat (limited to 'test-suite/kernel')
-rw-r--r--test-suite/kernel/inds.mv3
1 files changed, 0 insertions, 3 deletions
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.