From 656bcd55ed04c437bce26fd6db47c58a136b4ee6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2014 08:50:44 -0700 Subject: [PATCH] fix(frontends/lean): save 'choice' position Signed-off-by: Leonardo de Moura --- src/frontends/lean/calc.cpp | 2 +- src/frontends/lean/parser.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index e96538e29..713ede488 100644 --- a/src/frontends/lean/calc.cpp +++ b/src/frontends/lean/calc.cpp @@ -317,6 +317,6 @@ expr parse_calc(parser & p) { buffer choices; for (auto const & s : steps) choices.push_back(step_proof(s)); - return mk_choice(choices.size(), choices.data()); + return p.save_pos(mk_choice(choices.size(), choices.data()), pos); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index b3d380070..0f59206db 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -803,7 +803,7 @@ expr parser::parse_notation(parse_table t, expr * left) { expr r = instantiate_rev(copy_with_new_pos(a, p), args.size(), args.data()); cs.push_back(r); } - return mk_choice(cs.size(), cs.data()); + return save_pos(mk_choice(cs.size(), cs.data()), p); } expr parser::parse_nud_notation() {