Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

1 files changed, 16 insertions, 1 deletions

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.