From 7ca882d69a27ff5d688500012c97948ba9b06357 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Mar 2015 17:05:41 -0700 Subject: [PATCH] fix(frontends/lean/parse_rewrite_tactic): esimp error message position information --- src/frontends/lean/parse_rewrite_tactic.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index d221856e4..731a48027 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -145,13 +145,14 @@ expr parse_rewrite_tactic(parser & p) { expr parse_esimp_tactic(parser & p) { buffer elems; + auto pos = p.pos(); if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) { - elems.push_back(parse_rewrite_unfold(p)); + elems.push_back(p.save_pos(parse_rewrite_unfold(p), pos)); } else if (p.curr_is_token(get_lcurly_tk())) { - elems.push_back(parse_rewrite_unfold_core(p)); + elems.push_back(p.save_pos(parse_rewrite_unfold_core(p), pos)); } else { location loc = parse_tactic_location(p); - elems.push_back(mk_rewrite_reduce(loc)); + elems.push_back(p.save_pos(mk_rewrite_reduce(loc), pos)); } return mk_rewrite_tactic_expr(elems); }