From e778e3faecbb573b215b97d64c2b6a9d61bfca76 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Aug 2014 12:35:14 -0700 Subject: [PATCH] fix(tests/lean): adjust tests expected output Signed-off-by: Leonardo de Moura --- tests/lean/t3.lean.expected.out | 2 +- tests/lean/t9.lean.expected.out | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out index 5f450be553..7c65a357fd 100644 --- a/tests/lean/t3.lean.expected.out +++ b/tests/lean/t3.lean.expected.out @@ -10,7 +10,7 @@ Type Type Type t3.lean:26:10: error: invalid namespace declaration, atomic identifier expected -t3.lean:27:1: error: invalid declaration name 'full.name.U', identifier must be atomic +t3.lean:27:0: error: invalid declaration name 'full.name.U', identifier must be atomic Type Type t3.lean:35:2: error: universe level alias 'u' shadows existing global universe level diff --git a/tests/lean/t9.lean.expected.out b/tests/lean/t9.lean.expected.out index 15f8587be1..e02d98ed3e 100644 --- a/tests/lean/t9.lean.expected.out +++ b/tests/lean/t9.lean.expected.out @@ -1,3 +1,3 @@ add a (mul b a) : N -t9.lean:16:8: error: invalid expression +t9.lean:16:7: error: invalid expression add a (mul b a) : N