aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-03-15 18:39:48 +0100
committerPierre-Marie Pédrot2021-01-04 14:01:45 +0100
commitfd50f21cfe2460fa35fe962390f4ba810d7ca837 (patch)
treeaa8ac4dbae7e148bb6d383d439d225640ac3d86e /test-suite
parent0d7365e6ddcbd14933fcedae777649d31fb311cc (diff)
Temporarily deactivating printing check for cases.
Destruct has changed semantics, but I'd like to see how CI fares so far.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/Cases.out9
1 files changed, 5 insertions, 4 deletions
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: