From 2e4bc1ce29c52ae6e0625bef9a6905a70c0e6e89 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 23 Sep 2003 10:26:45 +0000
Subject: test d'implicite incorrect depuis que eq porte sur Type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4455 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/failure/check.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v
index 77f2252b88..0bf7091c13 100644
--- a/test-suite/failure/check.v
+++ b/test-suite/failure/check.v
@@ -1,3 +1,3 @@
 Implicits eq [1].
 
-Check (eq bool).
\ No newline at end of file
+Check (eq bool true).
-- 
cgit v1.2.3