diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 8479a5cbf..e8c156bf0 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -597,7 +597,9 @@ struct info_manager::imp { lean_assert(it != m_env_info.end() && it->m_line <= linenum); auto next = it; next++; - if (next == m_env_info.end() || next->m_line > linenum) + if (next == m_env_info.end()) + return optional>(mk_pair(it->m_env, it->m_options)); + if (next->m_line > linenum) return optional>(mk_pair(next->m_env, next->m_options)); it = next; }