From 00978cddf6e2da71892de6362e69c372429e159f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 19 Oct 2016 17:20:06 +0200
Subject: Test for variant of #5142 (good error message on pattern-matching
 failure).

---
 test-suite/output/Cases.out | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite/output/Cases.out')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 95fcd362e..8ce6f9795 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -59,3 +59,16 @@ end
 The command has indeed failed with message:
 Non exhaustive pattern-matching: no clause found for pattern 
 gadtTy _ _
+The command has indeed failed with message:
+In environment
+texpDenote : forall t : type, texp t -> typeDenote t
+t : type
+e : texp t
+t1 : type
+t2 : type
+t0 : type
+b : tbinop t1 t2 t0
+e1 : texp t1
+e2 : texp t2
+The term "0" has type "nat" while it is expected to have type
+ "typeDenote t0".
-- 
cgit v1.2.3