2 files changed, 28 insertions, 50 deletions
diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v
index 7ab720f6..97cef9a5 100644
--- a/contrib/subtac/test/ListDep.v
+++ b/contrib/subtac/test/ListDep.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import List.
 Require Import Coq.subtac.Utils.
 
@@ -21,63 +22,25 @@ Section Map_DependentRecursor.
   Variable l : list U.
   Variable f : { x : U | In x l } -> V.
 
+  Obligations Tactic := unfold sub_list in * ; 
+    subtac_simpl ; intuition.
+
   Program Fixpoint map_rec ( l' : list U | sub_list l' l )
-    { measure l' length } : { r : list V | length r = length 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.
     
-    Obligation 1.
-    intros.
-    destruct tl' ; simpl ; simpl in e.
-    subst x0 tl0.
-    rewrite <- Heql'.
-    rewrite e.
-    auto.
-    Qed.
-
-    Obligation 2.
-    simpl.
-    intros.
-    destruct l'.
-    simpl in Heql'.
-    destruct x0 ; simpl ; try discriminate.
-    inversion Heql'.
-    inversion s.
-    apply H.
-    auto with datatypes.
-    Qed.
-
-
-    Obligation 3 of map_rec.
-    simpl.
-    intros.
-    rewrite <- Heql'.
+  Next Obligation.
+    destruct_call map_rec.
+    simpl in *.
+    subst l'.
     simpl ; auto with arith.
-    Qed.
-
-    Obligation 4.
-    simpl.
-    intros.
-    destruct l'.
-    simpl in Heql'.
-    destruct x0 ; simpl ; try discriminate.
-    inversion Heql'.
-    subst x tl.
-    apply sub_list_tl with u ; auto.
-    Qed.
-  
-    Obligation 5.
-    intros.
-    rewrite <- Heql' ; auto.
-    Qed.
-    
-    Program Definition map : list V := map_rec l.
-    Obligation 1.
-      split ; auto.
-    Qed.
+  Qed.
+      
+  Program Definition map : list V := map_rec l.
     
 End Map_DependentRecursor.
 
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index b8d13fe6..3ceea173 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -70,7 +70,22 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    inversion l0.
+    intros.
+    inversion H.
   Defined.
+
+  Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := 
+    match l, n with
+      | hd :: _, 0 => hd
+      | _ :: tl, S n' => nth' tl n'
+      | nil, _ => !
+    end.
+
+  Next Obligation.
+  Proof.
+    intros.
+    inversion H.
+  Defined.
+
 End Nth.