1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 2b828d382..8ce6f9795 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -56,3 +56,19 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
+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".