From d7fc571e36686fe2b17559290db989c1e79a7db6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Mon, 5 Jun 2017 16:00:08 -0400 Subject: [PATCH] fix(library/init/meta): show_goal also changes the goal --- library/init/meta/interactive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 163fbab2f6..0528611593 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -906,7 +906,7 @@ tactic.done private meta def show_goal_aux (p : pexpr) : list expr → list expr → tactic unit | [] r := fail "show_goal tactic failed" | (g::gs) r := do - do {set_goals [g], g_ty ← target, ty ← i_to_expr p, unify g_ty ty >> set_goals (g :: r.reverse ++ gs) } + do {set_goals [g], g_ty ← target, ty ← i_to_expr p, unify g_ty ty, set_goals (g :: r.reverse ++ gs), tactic.change ty} <|> show_goal_aux gs (g::r)