diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/refine.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 47453b9ca7..96fa79ebd4 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -53,3 +53,11 @@ Refine [n] Cases i of 0 => ? | (S _) => ? end }. Abort. +(* Submitted by Roland Zumkeller (bug #931) *) +(* Don't turn dependent evar into metas *) + +Goal ((n:nat)n=O->Prop) -> Prop. +Intro P. +Refine(P ? ?). +Reflexivity. +Abort. |