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