From 34ea06f2f31cebf00bc7620fac34d963afe6a1dc Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 15 Dec 2015 14:54:07 +0100
Subject: Fix test-suite files after change in refine tactic.

Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
---
 test-suite/success/refine.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/success')

diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 1e667884b8..352abb2af5 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -62,7 +62,7 @@ Abort.
 Goal (forall n : nat, n = 0 -> Prop) -> Prop.
 intro P.
  refine (P _ _).
-2:reflexivity.
+reflexivity.
 Abort.
 
 (* Submitted by Jacek Chrzaszcz (bug #1102) *)
-- 
cgit v1.2.3