aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Cases.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Cases.out')
-rw-r--r--test-suite/output/Cases.out4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f846f4ee1..f44465456 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -47,10 +47,10 @@ foo' = if A 0 then true else false
f =
fun H : B =>
match H with
-| AC H0 =>
+| 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) H0
+ else fun _ : P false => Logic.I) x
end
: B -> True