From aed9a88b38d81a3ac2b7e3e138ec51f331a5e2bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 26 Oct 2014 10:19:44 -0700
Subject: [PATCH] fix(frontends/lean/parser): save identifier info for undef
 local

---
 src/frontends/lean/parser.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index f3e527285..25d7aba1b 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1077,6 +1077,8 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
     if (is_constant(*r)) {
         add_ref_index(const_name(*r), p);
         save_identifier_info(p, const_name(*r));
+    } else if (is_local(*r)) {
+        save_identifier_info(p, local_pp_name(*r));
     }
     return *r;
 }