diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 14:03:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 14:03:53 +0000 |
| commit | c078cba1208255cd2a2f5b60b6d10cb85b6e9cb2 (patch) | |
| tree | 60aa5f91bb15aa0eefcd7ae89cad1270ab04c273 /test-suite/success/refine.v | |
| parent | 71f451ca817decc4e5d59faeae38d0baa2bffd4a (diff) | |
Ajout bug #888
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6417 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/refine.v')
| -rw-r--r-- | test-suite/success/refine.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index acd9cf142..bc81462bf 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -30,10 +30,26 @@ Refine [l]<[l]l=l> end. Abort. +(* Submitted by Roland Zumkeller (bug #888) *) + +(* The Fix and CoFix rules expect a subgoal even for closed components of the + (co-)fixpoint *) + +Goal nat -> nat. +Refine( + Fix f {f [n:nat] : nat := (S ?) with + pred [n:nat] : nat := n}). +Intro; Exact 0. +Qed. + (* Submitted by Roland Zumkeller (bug #889) *) +(* The types of metas were in metamap and they were not updated when + passing through a binder *) + Goal (n:nat) nat -> n=0. Refine [n] Fix f { f [i:nat] : n=0 := Cases i of 0 => ? | (S _) => ? end }. Abort. + |