aboutsummaryrefslogtreecommitdiff
path: root/test-suite/vi/simple.v
diff options
context:
space:
mode:
authorEnrico Tassi2015-01-06 18:09:26 +0100
committerEnrico Tassi2015-01-06 18:09:35 +0100
commit341909bbc5c1c59e81dfad2f2532602e2561ec36 (patch)
tree28fb527cb921b4e02d4722549a24f6e2366f5c76 /test-suite/vi/simple.v
parentbf16900f43c1291136673e7614587fe51eebc88f (diff)
rename: vi -> vio
Diffstat (limited to 'test-suite/vi/simple.v')
-rw-r--r--test-suite/vi/simple.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/vi/simple.v b/test-suite/vi/simple.v
deleted file mode 100644
index 407074c1e7..0000000000
--- a/test-suite/vi/simple.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Lemma simple : True.
-Proof using. trivial. Qed.