max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(frontends/lean/elaborator): try to make error positions a bit more accurate

Browse source
This commit is contained in:
Sebastian Ullrich 2018-09-25 14:48:57 -07:00
parent bba8beca63
commit 11259b62d2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -3635,7 +3635,7 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
if (expected_type) tout() << "expected type:\n" << instantiate_mvars(*expected_type) << "\n";);
expr e2 = recover_expr_from_exception(expected_type, e, [&] () -> expr {
if (auto p = get_pos(e)) {
m_last_pos = p;
flet<optional<pos_info>> _(m_last_pos, p);
return visit(unwrap_pos(e), expected_type);
} else if (is_placeholder(e)) {
return visit_placeholder(e, expected_type);