From 11259b62d27998d830520fb79ce5714656d16d96 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 25 Sep 2018 14:48:57 -0700
Subject: [PATCH] chore(frontends/lean/elaborator): try to make error positions
 a bit more accurate

---
 src/frontends/lean/elaborator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 68f85c34a2..9376e4b7dd 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -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);