diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-17 18:11:56 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-17 18:11:56 +0000 |
commit | cc65a9b7754e9645ac72e629ce0b31359d8814cc (patch) | |
tree | a71845c38f16789be10679b1f00a04207511102d /contrib/subtac/test | |
parent | 54edcf4a4dbddbdf2a17a3dab2b4c244a5cd7db0 (diff) |
Correct implementation of undo in obligations handling code, correct some bugs in pattern-matching
compilation with multiple matched objects.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/test')
-rw-r--r-- | contrib/subtac/test/ListsTest.v | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v index b8d13fe6b..3ceea173f 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. |