From 299751982b87b39ac80cff77e65dca2f2ba0842c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Jan 2017 13:12:51 -0800 Subject: [PATCH] fix(frontends/lean/tactic_evaluator): 'begin [smt] ... end' block nested in regular one --- src/frontends/lean/tactic_evaluator.cpp | 2 +- tests/lean/smt_begin_end1.lean.expected.out | 11 ++++------- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/src/frontends/lean/tactic_evaluator.cpp b/src/frontends/lean/tactic_evaluator.cpp index 2606027b10..919d2cc0f3 100644 --- a/src/frontends/lean/tactic_evaluator.cpp +++ b/src/frontends/lean/tactic_evaluator.cpp @@ -151,7 +151,7 @@ tactic_state tactic_evaluator::execute_begin_end(tactic_state const & s, buffer< get_begin_end_block_elements(tactic, nested_tactics); new_s = execute_begin_end(new_s, nested_tactics, curr_ref); } else if (is_smt_begin_end_block(tactic)) { - new_s = execute_smt_begin_end(s, tactic, ref); + new_s = execute_smt_begin_end(new_s, tactic, curr_ref); } else { throw elaborator_exception(curr_ref, "ill-formed 'begin ... end' tactic block"); } diff --git a/tests/lean/smt_begin_end1.lean.expected.out b/tests/lean/smt_begin_end1.lean.expected.out index 0fd26de0b7..3f023d9132 100644 --- a/tests/lean/smt_begin_end1.lean.expected.out +++ b/tests/lean/smt_begin_end1.lean.expected.out @@ -5,10 +5,7 @@ h : p (f a) (f a) facts: {p (f a) (f a), p (f a) (f b), a = b} equalities: {{b, a}, {f a, f b}} ⊢ p a b -a b c : ℕ, -a_1 : a = b, -a_2 : p (f a) (f b), -h₁ : p (f a) (f a) -facts: {p (f a) (f a), p (f a) (f b), a = b} -equalities: {{b, a}, {f a, f b}} -⊢ p a b +a c : ℕ, +a_1 h₁ : p (f a) (f a) +facts: {p (f a) (f a)} +⊢ p a a