From 298bdfdcdebc2d0f18fbcce181cab4e05fcecce9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Dec 2020 11:19:58 -0800
Subject: [PATCH] fix: `focus` behavior

---
 src/Lean/Elab/Tactic/Basic.lean     | 10 +++++-----
 src/Lean/Elab/Tactic/Induction.lean |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 70b6dae333..af20fee660 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -213,7 +213,7 @@ def done : TacticM Unit := do
 
 @[builtinTactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ => done
 
-def focusAux {α} (tactic : TacticM α) : TacticM α := do
+def focus {α} (tactic : TacticM α) : TacticM α := do
   let (g, gs) ← getMainGoal
   setGoals [g]
   let a ← tactic
@@ -221,8 +221,8 @@ def focusAux {α} (tactic : TacticM α) : TacticM α := do
   setGoals (gs' ++ gs)
   pure a
 
-def focus {α} (tactic : TacticM α) : TacticM α :=
-  focusAux do let a ← tactic; done; pure a
+def focusAndDone {α} (tactic : TacticM α) : TacticM α :=
+  focus do let a ← tactic; done; pure a
 
 /- Close the main goal using the given tactic. If it fails, log the error and `admit` -/
 def closeUsingOrAdmit (tac : Syntax) : TacticM Unit := do
@@ -280,7 +280,7 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
   stx[0].forArgsM fun seqElem => evalTactic seqElem[0]
 
 @[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx =>
-  withRef stx[2] $ focus $ stx[1].forArgsM fun seqElem => evalTactic seqElem[0]
+  withRef stx[2] $ focusAndDone $ stx[1].forArgsM fun seqElem => evalTactic seqElem[0]
 
 @[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx =>
   focus $ evalTactic stx[1]
@@ -290,7 +290,7 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
   let mut gsNew := []
   for g in gs do
     setGoals [g]
-    focus <| evalTactic stx[1]
+    evalTactic stx[1]
     gsNew := gsNew ++ (← getUnsolvedGoals)
   setGoals gsNew
 
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 069ce67c70..b39d820a9e 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -430,7 +430,7 @@ private def generalizeTerm (term : Expr) : TacticM Expr := do
       let (fvarId, mvarId) ← Meta.intro1 mvarId
       pure (mkFVar fvarId, [mvarId])
 
-@[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx => focusAux do
+@[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx => focus do
   let targets ← stx[1].getSepArgs.mapM fun target => do
     let target ← withMainMVarContext $ elabTerm target none
     generalizeTerm target
@@ -548,7 +548,7 @@ def evalCasesUsing (elimId : Syntax) (targetRef : Syntax) (targets : Array Expr)
       assignExprMVar mvarId result.elimApp
       ElimApp.evalAlts elimInfo result.alts (getAltsOfOptInductionAlts optInductionAlts) (numEqs := targets.size)
 
-@[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx => focusAux do
+@[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx => focus do
   -- parser! nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
   let targets ← elabTargets stx[1].getSepArgs
   let optInductionAlts := stx[3]