From 7d7d15f8f7a7daf7bc13be7f85cd3e29bd30baae Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 19 Nov 2018 15:28:23 +0100
Subject: [PATCH] chore(frontends/lean/elaborator): improve error positions

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

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3d118d9285..520e9e5de3 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2003,6 +2003,7 @@ expr elaborator::visit_app(expr const & e, optional<expr> const & expected_type)
         return visit_scope_trace(e, expected_type);
     buffer<expr> args;
     expr const & fn = get_app_args(e, args);
+    flet<optional<pos_info>> _(m_last_pos, get_pos(fn));
     expr ufn = unwrap_pos(fn);
     if (is_infix_function(ufn)) {
         expr infix_fn = get_annotation_arg(ufn);