From 1f7fd3c91d41d661587c90f10cacba4728f38dfc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 16 Oct 2014 17:30:42 +0200
Subject: Fix test-suite scripts.

---
 test-suite/bugs/closed/3618.v | 2 +-
 test-suite/bugs/closed/3710.v | 4 +---
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/test-suite/bugs/closed/3618.v b/test-suite/bugs/closed/3618.v
index bbce32e9e4..dc560ad525 100644
--- a/test-suite/bugs/closed/3618.v
+++ b/test-suite/bugs/closed/3618.v
@@ -98,6 +98,6 @@ Admitted.
 (* To avoid looping class resolution *)
 Hint Mode IsEquiv - - + : typeclass_instances. 
 
-Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse}
+Fail Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse}
            (P Q : Type) {Q_inO : inO_internal Q}
 : IsEquiv (fun f : O P -> P => compose f (O_unit P)) := _.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3710.v b/test-suite/bugs/closed/3710.v
index 867e31ddf9..b9e2798d88 100644
--- a/test-suite/bugs/closed/3710.v
+++ b/test-suite/bugs/closed/3710.v
@@ -45,6 +45,4 @@ Context `{P : PreCategory -> Type}.
 Local Notation cat := (@sub_pre_cat P).
 Goal forall (s d d' : cat) (m1 : morphism cat d d') (m2 : morphism cat s d),
        NaturalIsomorphism (m1 o m2) (m1 o m2)%functor.
-  exact (fun _ _ _ _ _ => reflexivity _).
-(* Toplevel input, characters 15-54:
-Anomaly: variable o unbound. Please report. *)
\ No newline at end of file
+Fail exact (fun _ _ _ _ _ => reflexivity _).
-- 
cgit v1.2.3