summaryrefslogtreecommitdiff
path: root/plugins/subtac/test/Test1.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/subtac/test/Test1.v
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/subtac/test/Test1.v')
-rw-r--r--plugins/subtac/test/Test1.v16
1 files changed, 0 insertions, 16 deletions
diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v
deleted file mode 100644
index 7e0755d5..00000000
--- a/plugins/subtac/test/Test1.v
+++ /dev/null
@@ -1,16 +0,0 @@
-Program Definition test (a b : nat) : { x : nat | x = a + b } :=
- ((a + b) : { x : nat | x = a + b }).
-Proof.
-intros.
-reflexivity.
-Qed.
-
-Print test.
-
-Require Import List.
-
-Program hd_opt (l : list nat) : { x : nat | x <> 0 } :=
- match l with
- nil => 1
- | a :: l => a
- end.