michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/parser): save identifier info for undef local

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-26 10:19:44 -07:00
parent 8e6de93394
commit aed9a88b38
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1077,6 +1077,8 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
if (is_constant(*r)) { if (is_constant(*r)) {
add_ref_index(const_name(*r), p); add_ref_index(const_name(*r), p);
save_identifier_info(p, const_name(*r)); save_identifier_info(p, const_name(*r));
} else if (is_local(*r)) {
save_identifier_info(p, local_pp_name(*r));
} }
return *r; return *r;
} }