From 16ec9db1fc9360fc3396d3bd3af54d9df81e82b8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Sep 2020 13:12:00 -0700 Subject: [PATCH] chore: fix test --- tests/lean/shadow.lean.expected.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out index 266cf62c38..ef0810763b 100644 --- a/tests/lean/shadow.lean.expected.out +++ b/tests/lean/shadow.lean.expected.out @@ -1,11 +1,11 @@ shadow.lean:4:0: error: type mismatch h has type - x._shadowed.1=x._shadowed.1 + x✝¹=x✝¹ but it is expected to have type x=x failed to synthesize instance - CoeT (x._shadowed.1=x._shadowed.1) _ (x=x) + CoeT (x✝¹=x✝¹) _ (x=x) shadow.lean:9:0: error: type mismatch h has type