1 files changed, 34 insertions, 0 deletions
diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v
new file mode 100644
index 00000000..90ae8bae
--- /dev/null
+++ b/plugins/subtac/test/take.v
@@ -0,0 +1,34 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
+Require Import JMeq.
+Require Import List.
+Require Import Program.
+
+Set Implicit Arguments.
+Obligations Tactic := idtac.
+
+Print cons.
+
+Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
+  match n with
+  | 0 => nil
+  | S p =>
+    match l with
+    | cons hd tl => let rest := take tl p in cons hd rest
+    | nil => !
+    end
+  end.
+
+Require Import Omega.
+Solve All Obligations.
+Next Obligation.
+  destruct_call take ; program_simpl.
+Defined.
+
+Next Obligation.
+  intros.
+  inversion H.
+Defined.
+
+
+
+