From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/success/refine.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'test-suite/success/refine.v') diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 4d743a6d..1e667884 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -62,14 +62,14 @@ Abort. Goal (forall n : nat, n = 0 -> Prop) -> Prop. intro P. refine (P _ _). -reflexivity. +2: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 +(* 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. @@ -84,7 +84,7 @@ Definition div : refine (fun m div_rec n => match div_rec m n with - | exist _ _ => _ + | exist _ _ _ => _ end). Abort. -- cgit v1.2.3