From 9993ac283e14c0f789b9fa826fd20086059cdcd8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 13 Jan 2015 06:43:53 +0530
Subject: Fix test-suite file, we were testing that no anomaly was raised and
 this is the case now.

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

diff --git a/test-suite/bugs/closed/3417.v b/test-suite/bugs/closed/3417.v
index 2931fbda52..9d7c6f013d 100644
--- a/test-suite/bugs/closed/3417.v
+++ b/test-suite/bugs/closed/3417.v
@@ -3,5 +3,5 @@ Require Setoid.
 Goal forall {T}(a b : T), b=a -> {c | c=b}.
 Proof.
 intros T a b H.
-setoid_rewrite H.
+try setoid_rewrite H.
 Abort.
-- 
cgit v1.2.3