Imported Upstream version 8.5~beta1+dfsg

1 files changed, 5 insertions, 5 deletions

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.