fix(library/init/meta/tactic): typo

2016-06-21 08:19:39 -07:00 · 2016-06-21 08:19:39 -07:00 · 0663733d27
commit 0663733d27
parent 4f7f59e47f
1 changed files with 1 additions and 1 deletions
--- 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