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