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

fix(frontends/lean/parser): missing identifier information, fixes #83

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-21 16:58:04 -07:00
parent 2071a5986f
commit 3498d7ad61
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -980,10 +980,6 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p));
}
r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
if (is_constant(*r)) {
add_ref_index(const_name(*r), p);
save_identifier_info(p, const_name(*r));
}
save_overload(*r);
}
if (!r && m_no_undef_id_error)
@ -991,6 +987,10 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
if (!r)
throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
save_type_info(*r);
if (is_constant(*r)) {
add_ref_index(const_name(*r), p);
save_identifier_info(p, const_name(*r));
}
return *r;
}