Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 38 insertions, 0 deletions

diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
new file mode 100644
index 00000000..87ab47d6
--- /dev/null
+++ b/contrib/subtac/test/take.v
@@ -0,0 +1,38 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
+Require Import JMeq.
+Require Import List.
+Require Import Coq.subtac.Utils.
+
+Set Implicit Arguments.
+
+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.
+
+Next Obligation.
+  intros.
+  simpl in l0.
+  apply le_S_n ; exact l0.
+Defined.
+
+Next Obligation.
+  intros.
+  destruct_call take ; subtac_simpl.
+Defined.
+
+Next Obligation.
+  intros.
+  inversion l0.
+Defined.
+
+
+
+