From a20b1beea481acb78992ffa3bdf5ef91772227e9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 14:04:35 -0700
Subject: [PATCH] chore: cleanup

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

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 3839c6a30a..ba6726fdf7 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -26,33 +26,14 @@ def ensureAssignmentHasNoMVars (mvarId : MVarId) : TermElabM Unit := do
 val ← instantiateMVars (mkMVar mvarId);
 when val.hasExprMVar $ throwError ("tactic failed, result still contain metavariables" ++ indentExpr val)
 
-private partial def getTacticRCurly? : Syntax → Option Syntax
-| stx =>
-  if stx.isOfKind `Lean.Parser.Term.byTactic then
-    getTacticRCurly? $ stx.getArg 1
-  else if stx.isOfKind `Lean.Parser.Tactic.seq && stx.getArgs.size == 1 then
-    getTacticRCurly? $ stx.getArg 0
-  else if stx.isOfKind `Lean.Parser.Tactic.nestedTacticBlockCurly then
-    some (stx.getArg 2)
-  else
-    none
-
-private def getTacticErrorRef (tacticCode : Syntax) : TermElabM Syntax := do
-ref ← getRef;
-match getTacticRCurly? tacticCode with
-| some rcurly => pure $ replaceRef rcurly ref
-| none        => pure $ replaceRef tacticCode ref
-
 def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
 /- Recall, `tacticCode` is the whole `by ...` expression.
    We store the `by` because in the future we want to save the initial state information at the `by` position. -/
 let code := tacticCode.getArg 1;
 modifyThe Meta.State $ fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId };
 remainingGoals ← liftTacticElabM mvarId $ do { evalTactic code; getUnsolvedGoals };
-ref ← getTacticErrorRef tacticCode;
-withRef ref do
-  unless remainingGoals.isEmpty (reportUnsolvedGoals remainingGoals);
-  ensureAssignmentHasNoMVars mvarId
+unless remainingGoals.isEmpty (reportUnsolvedGoals remainingGoals);
+ensureAssignmentHasNoMVars mvarId
 
 /-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
 private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 22d30107a1..4e13299ee6 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -379,8 +379,8 @@ fun stx => match_syntax stx with
 @[builtinTactic paren] def evalParen : Tactic :=
 fun stx => evalTactic (stx.getArg 1)
 
-@[builtinTactic tacticSeq1Bracketed] def evalTacticSeq1Bracketed : Tactic :=
-fun stx => focus $ (stx.getArg 1).forSepArgsM evalTactic
+@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
+fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic
 
 /--
   First method searches for a metavariable `g` s.t. `tag` is a suffix of its name.