From c61e5783458d4b9f2cd104bd027893f6bdc82ded Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 18 Aug 2014 16:43:40 +0200
Subject: Fix test-suite file.

---
 test-suite/bugs/opened/3377.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test-suite/bugs/opened/3377.v b/test-suite/bugs/opened/3377.v
index 9ad3779d16..23c0a965c8 100644
--- a/test-suite/bugs/opened/3377.v
+++ b/test-suite/bugs/opened/3377.v
@@ -1,4 +1,5 @@
 Set Primitive Projections.
+Set Implicit Arguments.
 Record prod A B := pair { fst : A; snd : B}.
 
 Goal fst (@pair Type Type Type Type).
-- 
cgit v1.2.3