max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/meta): show_goal also changes the goal

Browse source
This commit is contained in:
Johannes Hölzl 2017-06-05 16:00:08 -04:00 • committed by Leonardo de Moura
parent 544817cf15
commit d7fc571e36
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/interactive.lean
View file

@ -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)