From 62d343be2ed5e987b09ffe2c3532883d626d94d1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Dec 2014 20:05:54 +0100
Subject: Fixing test-suite.

---
 test-suite/bugs/closed/3417.v | 2 +-
 test-suite/bugs/closed/3487.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/test-suite/bugs/closed/3417.v b/test-suite/bugs/closed/3417.v
index 19a1863e0a..2931fbda52 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.
-Fail setoid_rewrite H.
+setoid_rewrite H.
 Abort.
diff --git a/test-suite/bugs/closed/3487.v b/test-suite/bugs/closed/3487.v
index ba7a5c98fc..03c60a8baa 100644
--- a/test-suite/bugs/closed/3487.v
+++ b/test-suite/bugs/closed/3487.v
@@ -5,4 +5,4 @@ Instance: baz.
 Admitted.
 Definition baz0 := ((_ : baz) = (_ : baz)).
 Definition foo1 := (foo = foo).
-Fail Definition baz1 := prod ((_ : baz) = (_ : baz)) (foo = foo).
+Definition baz1 := prod ((_ : baz) = (_ : baz)) (foo = foo).
-- 
cgit v1.2.3