From f9c2d5d26a6a8e15549ada1f69d630acfa1a9437 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Feb 2015 13:39:27 +0100
Subject: Fixing test-suite.

---
 test-suite/bugs/closed/4017.v | 2 ++
 test-suite/bugs/closed/4018.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v
index a6f177b496..aa810f4f0e 100644
--- a/test-suite/bugs/closed/4017.v
+++ b/test-suite/bugs/closed/4017.v
@@ -1,3 +1,5 @@
+Set Implicit Arguments.
+
 (* Use of implicit arguments was lost in multiple variable declarations *)
 Variables 
   (A1 : Type)
diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v
index c3a045943c..8895e09e02 100644
--- a/test-suite/bugs/closed/4018.v
+++ b/test-suite/bugs/closed/4018.v
@@ -1,3 +1,3 @@
 (* Catching PatternMatchingFailure was lost at some point *)
 Goal nat -> True.
-intros [=].
+Fail intros [=].
-- 
cgit v1.2.3