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

fix(frontends/lean/parser): add missing save_pos

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 10:32:43 -07:00
parent 6ec5d768d0
commit 0791c83731
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -818,10 +818,10 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
for (auto const & e : as) {
new_as.push_back(copy_with_new_pos(propagate_levels(e, ls), p));
}
r = mk_choice(new_as.size(), new_as.data());
r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
}
if (m_no_undef_id_error)
r = mk_constant(get_namespace(m_env) + id, ls);
r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
if (!r)
throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
return *r;