diff options
| -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: |