From bebe8a4f173facac415785824587fcbbbb1daaba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Apr 2015 02:52:09 -0700 Subject: [PATCH] fix(tests/lean/bad_coercions): expected output --- tests/lean/bad_coercions.lean.expected.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/bad_coercions.lean.expected.out b/tests/lean/bad_coercions.lean.expected.out index 8d31bf5f5b..04ed19d551 100644 --- a/tests/lean/bad_coercions.lean.expected.out +++ b/tests/lean/bad_coercions.lean.expected.out @@ -1,2 +1,2 @@ -bad_coercions.lean:12:18: error: invalid '[coercion]' attribute, coercions cannot be defined in contexts -bad_coercions.lean:18:16: error: invalid '[coercion]' attribute, coercions cannot be defined in contexts +bad_coercions.lean:12:18: error: invalid '[coercion]' attribute, (non local) coercions cannot be defined in contexts +bad_coercions.lean:18:16: error: invalid '[coercion]' attribute, (non local) coercions cannot be defined in contexts