From c8ad5e94064d640f7957108469e77d3edb602afc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Mar 2015 13:43:33 -0800 Subject: [PATCH] feat(frontends/lean/builtin_exprs): focus on have-tactic goal --- src/frontends/lean/builtin_exprs.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 82a208fe7d..e726adda89 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -204,6 +204,8 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & auto pos = p.pos(); expr t = p.parse_expr(); t = p.mk_app(get_exact_tac_fn(), t, pos); + t = p.save_pos(mk_begin_end_element_annotation(t), pos); + t = p.save_pos(mk_begin_end_annotation(t), pos); add_tac(t, pos); } else if (p.curr_is_token(get_proof_tk())) { auto pos = p.pos(); @@ -211,6 +213,8 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & expr t = p.parse_expr(); p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected"); t = p.mk_app(get_exact_tac_fn(), t, pos); + t = p.save_pos(mk_begin_end_element_annotation(t), pos); + t = p.save_pos(mk_begin_end_annotation(t), pos); add_tac(t, pos); } else if (p.curr_is_token(get_begin_tk())) { auto pos = p.pos();