diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b8ec7ad255..bd229b4664 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1257,7 +1257,7 @@ public: if (!prev || p.first != prev->first) { auto out = regular(m_env, m_ios); flyinfo_scope info(out); - out << m_pos_provider->get_file_name() << ":" << p.first.first << ":" << p.first.second + out << m_pos_provider->get_file_name() << ":" << p.first.first << ":" << p.first.second+1 << ": type\n" << p.second << endl; prev = p; }