From 44b149ec1d220d38754545f18a39ef76a3be44b5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 Jun 2014 11:01:11 +0200
Subject: Fix test-suite script for HoTT coq bug #34

---
 test-suite/bugs/closed/HoTT_coq_034.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/bugs/closed/HoTT_coq_034.v b/test-suite/bugs/closed/HoTT_coq_034.v
index ae665931a8..8d5201f635 100644
--- a/test-suite/bugs/closed/HoTT_coq_034.v
+++ b/test-suite/bugs/closed/HoTT_coq_034.v
@@ -14,7 +14,7 @@ Module Short.
 
   Set Printing Universes.
   Check bar nat Set : Set. (* success *)
-  Fail Check foo nat Set : Set. (* Toplevel input, characters 6-17:
+  Check foo nat Set : Set. (* Toplevel input, characters 6-17:
 Error:
 The term "foo (* Top.303 Top.304 *) nat Set" has type
 "Type (* Top.304 *)" while it is expected to have type
-- 
cgit v1.2.3