diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 1229c10312..93a7d54012 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -227,7 +227,7 @@ do gs ← get_goals, tac, gs' ← get_goals, match gs' with - | [] := set_goals gs + | [] := set_goals rs | _ := fail "focus tactic failed, focused goal has not been solved" end end