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

fix(frontends/lean/parse_rewrite_tactic): esimp error message position information

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-12 17:05:41 -07:00
parent 026622a790
commit 7ca882d69a
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/parse_rewrite_tactic.cpp
View file

@ -145,13 +145,14 @@ expr parse_rewrite_tactic(parser & p) {
expr parse_esimp_tactic(parser & p) {
buffer<expr> 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);
}