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.