diff options
| author | Pierre-Marie Pédrot | 2019-03-15 18:39:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:01:45 +0100 |
| commit | fd50f21cfe2460fa35fe962390f4ba810d7ca837 (patch) | |
| tree | aa8ac4dbae7e148bb6d383d439d225640ac3d86e /test-suite | |
| parent | 0d7365e6ddcbd14933fcedae777649d31fb311cc (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.out | 9 |
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: |
