diff --git a/tests/lean/bad_inaccessible.lean.expected.out b/tests/lean/bad_inaccessible.lean.expected.out index 4494d7ed57..c1391f5dc3 100644 --- a/tests/lean/bad_inaccessible.lean.expected.out +++ b/tests/lean/bad_inaccessible.lean.expected.out @@ -4,4 +4,4 @@ bad_inaccessible.lean:7:7: error: invalid use of inaccessible term, the provided but is expected to be a bad_inaccessible.lean:15:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments - ?m_1 + 1 + .?m_1 + 1