From a6a87649c3e0ea205e0ad9e9536bb881ddc2e73b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 6 Dec 2013 11:04:35 +0100
Subject: Fix the refine related test-suite files to account for the new
 refine.

---
 test-suite/bugs/closed/931.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v
index 21f15e7218..e86b3be64e 100644
--- a/test-suite/bugs/closed/931.v
+++ b/test-suite/bugs/closed/931.v
@@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop.
 
 Goal Prop.
   refine (P _ _).
-  instantiate (1:=0).
+  2:instantiate (1:=0).
   trivial.
 Qed.
-- 
cgit v1.2.3