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

fix(frontends/lean/builtin_exprs): error position

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-20 15:56:58 -07:00
parent fd40999909
commit a3aca96cb9
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/builtin_exprs.cpp
View file

@ -130,8 +130,9 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
else
p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
if (p.curr_is_token(get_end_tk())) {
auto pos = p.pos();
p.next();
throw parser_error("invalid 'begin-end' expression, tactic or expression expected", p.pos());
throw parser_error("invalid 'begin-end' expression, tactic or expression expected", pos);
}
bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||