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