From 9fb15a33ba59b3543e1d277d7bf4b6bd2f69922d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Sep 2014 22:05:50 +0200
Subject: Fixing TestRefine test-suite file.

---
 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 213b528301..5bea53c947 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.
 
- refine (fix f (x : nat) : x = x := _).
+Fail refine (fix f (x : nat) : x = x := _).
 
 Restart.
 
-- 
cgit v1.2.3