From fb6dfa4af22cec70d84fc780edaf8c25e429b68c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jul 2020 12:36:33 -0700 Subject: [PATCH] chore: fix test --- tests/lean/private.lean.expected.out | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/private.lean.expected.out b/tests/lean/private.lean.expected.out index 51b52b82c4..913e3a898b 100644 --- a/tests/lean/private.lean.expected.out +++ b/tests/lean/private.lean.expected.out @@ -1,5 +1,5 @@ Bla.foo=="world" : Bool -private.lean:14:8: error: private declaration 'Bla.foo' has already been declared +private.lean:14:12: error: private declaration 'Bla.foo' has already been declared foo==0 : Bool Bla.foo : String Boo.Bla.boo=="world" : Bool @@ -9,5 +9,5 @@ Boo.boo==100 : Bool Boo.Bla.boo=="world" : Bool Boo.boo==100 : Bool Nat.mul10 x : Nat -private.lean:65:8: error: a non-private declaration 'y' has already been declared -private.lean:68:0: error: a private declaration 'z' has already been declared +private.lean:65:12: error: a non-private declaration 'y' has already been declared +private.lean:68:4: error: a private declaration 'z' has already been declared