3 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v
index 714df5cca..9e7d1eb5d 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 7c0133099..9e6107b30 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 4c7f9344e..da9290cba 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.