From ec9fda550cd997cc342e2f109cd6ceeadebec0e0 Mon Sep 17 00:00:00 2001
From: Xavier Clerc
Date: Tue, 25 Nov 2014 15:41:48 +0100
Subject: Tweak some test cases.

---
 test-suite/bugs/opened/3248.v | 2 +-
 test-suite/bugs/opened/3459.v | 2 +-
 test-suite/bugs/opened/3804.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v
index 714df5ccae..9e7d1eb5dd 100644
--- a/test-suite/bugs/opened/3248.v
+++ b/test-suite/bugs/opened/3248.v
@@ -13,5 +13,5 @@ Proof.
   intros A B x y.
   pose (f := fun (x y : A) => conj x y).
   pose (a := $(ret_and_left f)$).
-  unify (a x y) (conj x y).
+  Fail unify (a x y) (conj x y).
 Abort.
diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v
index 7c01330990..9e6107b30a 100644
--- a/test-suite/bugs/opened/3459.v
+++ b/test-suite/bugs/opened/3459.v
@@ -25,7 +25,7 @@ Variable x : nat.
 Goal True.
 evar (e : Prop).
 assert e.
-let r := constr:(eq_refl x) in clear x; exact r.
+Fail let r := constr:(eq_refl x) in clear x; exact r.
 Abort.
 
 End F.
diff --git a/test-suite/bugs/opened/3804.v b/test-suite/bugs/opened/3804.v
index 4c7f9344e4..da9290cbad 100644
--- a/test-suite/bugs/opened/3804.v
+++ b/test-suite/bugs/opened/3804.v
@@ -9,4 +9,4 @@ End Foo.
 Module Bar.
   Include Foo.
 End Bar.
-Fail Definition foo := eq_refl : Foo.T = Bar.T.
+Definition foo := eq_refl : Foo.T = Bar.T.
-- 
cgit v1.2.3