From c772d7bf84883e5fbb9a6a5e54a6a1272b3e2ab2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 28 Feb 2015 09:03:56 -0800 Subject: [PATCH] fix(frontends/lean/elaborator): unassigned metavariable when using nested begin-end blocks Closes #454 --- src/frontends/lean/elaborator.cpp | 12 +++++------- tests/lean/run/454.lean | 6 ++++++ 2 files changed, 11 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/454.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3bf523e9f..a4adb7f96 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1578,15 +1578,13 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr goals gs = ps.get_goals(); if (!gs) throw_elaborator_exception("invalid nested begin-end block, there are no goals to be solved", ptac); - goal g = head(gs); - expr mvar = g.get_mvar(); - proof_state focus_ps(ps, goals(g)); + goal g = head(gs); + expr mvar = g.get_mvar(); + name_generator ngen = ps.get_ngen(); + proof_state focus_ps(ps, goals(g), ngen.mk_child()); if (!try_using_begin_end(subst, mvar, focus_ps, ptac)) return false; - substitution ps_new_subst = ps.get_subst(); - name const & mvar_name = mlocal_name(mvar); - ps_new_subst.assign(mvar_name, *subst.get_expr(mvar_name)); - ps = proof_state(ps, tail(gs), ps_new_subst); + ps = proof_state(ps, tail(gs), subst, ngen); } else { expr new_ptac = subst.instantiate_all(ptac); if (auto tac = pre_tactic_to_tactic(new_ptac)) { diff --git a/tests/lean/run/454.lean b/tests/lean/run/454.lean new file mode 100644 index 000000000..f0ce488b5 --- /dev/null +++ b/tests/lean/run/454.lean @@ -0,0 +1,6 @@ +constants (A : Type₁) (P : A → Type₁) (H : Π{a b : A}, P a → P b) (a b : A) (K : P a) + +theorem foo : P b := +begin + apply H, {apply K} +end