1 files changed, 49 insertions, 0 deletions
diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v
new file mode 100644
index 00000000..e3dbd127
--- /dev/null
+++ b/plugins/subtac/test/ListDep.v
@@ -0,0 +1,49 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
+Require Import List.
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+
+Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l.
+
+Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'.
+Proof.
+  intros.
+  inversion H.
+  split.
+  intros.
+  apply H0.
+  auto with datatypes.
+  auto with arith.
+Qed.
+
+Section Map_DependentRecursor.
+  Variable U V : Set.
+  Variable l : list U.
+  Variable f : { x : U | In x l } -> V.
+
+  Obligations Tactic := unfold sub_list in * ;
+    program_simpl ; intuition.
+
+  Program Fixpoint map_rec ( l' : list U | sub_list l' l )
+    { measure length l' } : { r : list V | length r = length l' } :=
+    match l' with
+      | nil => nil
+      | cons x tl => let tl' := map_rec tl in
+	f x :: tl'
+    end.
+
+  Next Obligation.
+    destruct_call map_rec.
+    simpl in *.
+    subst l'.
+    simpl ; auto with arith.
+  Qed.
+
+  Program Definition map : list V := map_rec l.
+
+End Map_DependentRecursor.
+
+Extraction map.
+Extraction map_rec.
+