diff options
| -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 ad4eed5ae5..acd9cf1421 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. |