From 2aaa58c22e37b05e3637ac7161bb464da7db054a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Sep 2016 10:22:41 +0200
Subject: Fixing test-suite after commit 43104a0b.

---
 test-suite/success/TestRefine.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index c8a8b862fa..023cb5f59d 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -53,7 +53,7 @@ Abort.
 
 Lemma essai2 : forall x : nat, x = x.
 
-Fail refine (fix f (x : nat) : x = x := _).
+refine (fix f (x : nat) : x = x := _).
 
 Restart.
 
-- 
cgit v1.2.3