From fd50f21cfe2460fa35fe962390f4ba810d7ca837 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 Mar 2019 18:39:48 +0100
Subject: Temporarily deactivating printing check for cases.

Destruct has changed semantics, but I'd like to see how CI fares so far.
---
 test-suite/output/Cases.out | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 984ac4e527..6fd4d37ab4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -50,10 +50,11 @@ f =
 fun H : B =>
 match H with
 | AC x =>
-    let b0 := b in
-    (if b0 as b return (P b -> True)
-     then fun _ : P true => Logic.I
-     else fun _ : P false => Logic.I) x
+    (fun x0 : P b =>
+     let b0 := b in
+     (if b0 as b return (P b -> True)
+      then fun _ : P true => Logic.I
+      else fun _ : P false => Logic.I) x0) x
 end
      : B -> True
 The command has indeed failed with message:
-- 
cgit v1.2.3