diff options
author | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /test-suite/success/refine.v | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'test-suite/success/refine.v')
-rw-r--r-- | test-suite/success/refine.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index b61cf275..4346ce9a 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -64,3 +64,26 @@ intro P. refine (P _ _). reflexivity. Abort. + +(* Submitted by Jacek Chrzaszcz (bug #1102) *) + +(* le problème a été résolu ici par normalisation des evars présentes + dans les types d'evars, mais le problème reste a priori ouvert dans + le cas plus général d'evars non instanciées dans les types d'autres + evars *) + +Goal exists n:nat, n=n. +refine (ex_intro _ _ _). +Abort. + +(* Used to failed with error not clean *) + +Definition div : + forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) -> + forall n:nat, {q:nat | x = q*n}. +refine + (fun m div_rec n => + match div_rec m n with + | exist _ _ => _ + end). +Abort. |