diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-08 22:04:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-03-08 22:04:18 +0000 |
| commit | 845bd29d5705bae113afed6f5b8fd3195fb6b0fd (patch) | |
| tree | b8055d9d223bccdc1b48cd7cdc59ebcfb3dda737 /test-suite/success/refine.v | |
| parent | b2a962c342c74e96dc81e9eca30515282864620c (diff) | |
Fix bug #931: leave dependent evars as such for refine
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/refine.v')
| -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 47453b9ca..96fa79ebd 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. |