diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 13:10:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 13:10:10 +0000 |
| commit | 71f451ca817decc4e5d59faeae38d0baa2bffd4a (patch) | |
| tree | a036e48dc6d47269d7939b76701908984d6d589f | |
| parent | 9e1bc9aa4e2963a11ffd9a286a9e6319fe1cb5c6 (diff) | |
Ajout bug #889
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6416 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/refine.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index ad4eed5ae..acd9cf142 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -28,3 +28,12 @@ Refine [l]<[l]l=l> | (cons O l0) => ? | (cons (S _) l0) => ? end. +Abort. + +(* Submitted by Roland Zumkeller (bug #889) *) + +Goal (n:nat) nat -> n=0. +Refine [n] + Fix f { f [i:nat] : n=0 := + Cases i of 0 => ? | (S _) => ? end }. +Abort. |