From a3aca96cb97b95f565b585c2e1f424905545f637 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2014 15:56:58 -0700 Subject: [PATCH] fix(frontends/lean/builtin_exprs): error position --- src/frontends/lean/builtin_exprs.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 93aba87ac..b11ce3f12 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -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()) ||