diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index a6fe3117e3..68193d1803 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -8,35 +8,32 @@ import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assert
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.SyntheticMVars
+new_frontend
 
-namespace Lean
-namespace Elab
-namespace Tactic
-
+namespace Lean.Elab.Tactic
 open Meta
 
 /- `elabTerm` for Tactics and basic tactics that use it. -/
 
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr :=
 withRef stx $ liftTermElabM $ Term.withoutErrToSorry do
-  e ← Term.elabTerm stx expectedType?;
-  Term.synthesizeSyntheticMVars mayPostpone;
+  let e ← Term.elabTerm stx expectedType?
+  Term.synthesizeSyntheticMVars mayPostpone
   instantiateMVars e
 
 def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do
-e ← elabTerm stx expectedType? mayPostpone;
+let e ← elabTerm stx expectedType? mayPostpone
 ensureHasType expectedType? e
 
 @[builtinTactic «exact»] def evalExact : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| exact $e) => do
-    (g, gs) ← getMainGoal;
-    withMVarContext g $ do {
-      decl ← getMVarDecl g;
-      val  ← elabTermEnsuringType e decl.type;
-      ensureHasNoMVars val;
+    let (g, gs) ← getMainGoal
+    withMVarContext g do
+      let decl ← getMVarDecl g
+      let val  ← elabTermEnsuringType e decl.type
+      ensureHasNoMVars val
       assignExprMVar g val
-    };
     setGoals gs
   | _ => throwUnsupportedSyntax
 
@@ -44,19 +41,17 @@ fun stx => match_syntax stx with
 fun _ => `(tactic| exact sorry)
 
 def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
-val  ← elabTermEnsuringType stx expectedType?;
-newMVarIds ← getMVarsNoDelayed val;
-newMVarIds ←
-    if allowNaturalHoles then
-      pure newMVarIds.toList
-    else do {
-      naturalMVarIds ← newMVarIds.filterM fun mvarId => do { mvarDecl ← getMVarDecl mvarId; pure mvarDecl.kind.isNatural };
-      syntheticMVarIds ← newMVarIds.filterM fun mvarId => do { mvarDecl ← getMVarDecl mvarId; pure $ !mvarDecl.kind.isNatural };
-      liftM $ Term.logUnassignedUsingErrorInfos naturalMVarIds;
-      pure syntheticMVarIds.toList
-    };
-tag ← getMainTag;
-tagUntaggedGoals tag tagSuffix newMVarIds;
+let val ← elabTermEnsuringType stx expectedType?
+let newMVarIds ← getMVarsNoDelayed val
+let newMVarIds ←
+  if allowNaturalHoles then
+    pure newMVarIds.toList
+  else
+    let naturalMVarIds ← newMVarIds.filterM fun mvarId => do return (← getMVarDecl mvarId).kind.isNatural
+    let syntheticMVarIds ← newMVarIds.filterM fun mvarId => do return !(← getMVarDecl mvarId).kind.isNatural
+    Term.logUnassignedUsingErrorInfos naturalMVarIds
+    pure syntheticMVarIds.toList
+tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
 pure (val, newMVarIds)
 
 /- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
@@ -64,11 +59,11 @@ pure (val, newMVarIds)
    filled by typing constraints.
    "Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation `?<hole-name>`. -/
 def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : TacticM Unit := do
-(g, gs) ← getMainGoal;
+let (g, gs) ← getMainGoal
 withMVarContext g do
-  decl ← getMVarDecl g;
-  (val, gs') ← elabTermWithHoles stx decl.type tagSuffix allowNaturalHoles;
-  assignExprMVar g val;
+  let decl ← getMVarDecl g
+  let (val, gs') ← elabTermWithHoles stx decl.type tagSuffix allowNaturalHoles
+  assignExprMVar g val
   setGoals (gs ++ gs')
 
 @[builtinTactic «refine»] def evalRefine : Tactic :=
@@ -84,14 +79,13 @@ fun stx => match_syntax stx with
 @[builtinTactic Lean.Parser.Tactic.apply] def evalApply : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| apply $e) => do
-    (g, gs) ← getMainGoal;
-    gs' ← withMVarContext g $ do {
-      decl ← getMVarDecl g;
-      val  ← elabTerm e none true;
-      gs'  ← liftMetaM $ Meta.apply g val;
-      liftTermElabM $ Term.synthesizeSyntheticMVarsNoPostponing;
+    let (g, gs) ← getMainGoal
+    let gs' ← withMVarContext g do
+      let decl ← getMVarDecl g
+      let val  ← elabTerm e none true
+      let gs'  ← Meta.apply g val
+      Term.synthesizeSyntheticMVarsNoPostponing
       pure gs'
-    };
     -- TODO: handle optParam and autoParam
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
@@ -100,25 +94,21 @@ fun stx => match_syntax stx with
   Elaborate `stx`. If it a free variable, return it. Otherwise, assert it, and return the free variable.
   Note that, the main goal is updated when `Meta.assert` is used in the second case. -/
 def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId := do
-(mvarId, others) ← getMainGoal;
-withMVarContext mvarId $ do
-  e ← elabTerm stx none;
+let (mvarId, others) ← getMainGoal
+withMVarContext mvarId do
+  let e ← elabTerm stx none
   match e with
   | Expr.fvar fvarId _ => pure fvarId
-  | _ => do
-    type ← inferType e;
-    let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do {
-      (fvarId, mvarId) ← liftMetaM do {
-        mvarId ← Meta.assert mvarId userName type e;
+  | _ =>
+    let type ← inferType e
+    let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do
+      let (fvarId, mvarId) ← liftMetaM do
+        mvarId ← Meta.assert mvarId userName type e
         Meta.intro1Core mvarId preserveBinderNames
-      };
-      setGoals $ mvarId::others;
+      setGoals $ mvarId::others
       pure fvarId
-    };
     match userName? with
     | none          => intro `h false
     | some userName => intro userName true
 
-end Tactic
-end Elab
-end Lean
+end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean
index bb1923a0a5..8745396da1 100644
--- a/src/Lean/Elab/Tactic/Generalize.lean
+++ b/src/Lean/Elab/Tactic/Generalize.lean
@@ -7,11 +7,9 @@ import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Intro
 import Lean.Elab.Tactic.ElabTerm
+new_frontend
 
-namespace Lean
-namespace Elab
-namespace Tactic
-
+namespace Lean.Elab.Tactic
 open Meta
 
 private def getAuxHypothesisName (stx : Syntax) : Option Name :=
@@ -22,57 +20,55 @@ private def getVarName (stx : Syntax) : Name :=
 stx.getIdAt 4
 
 private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
-tag         ← Meta.getMVarTag mvarId;
-eType       ← inferType e;
-u           ← Meta.getLevel eType;
-mvar' ← Meta.mkFreshExprSyntheticOpaqueMVar target tag;
-let rfl    := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e;
-let val    := mkApp2 mvar' e rfl;
-assignExprMVar mvarId val;
-let mvarId' := mvar'.mvarId!;
-(_, mvarId') ← Meta.introNP mvarId' 2;
+let tag    ← Meta.getMVarTag mvarId
+let eType  ← inferType e
+let u      ← Meta.getLevel eType
+let mvar'  ← Meta.mkFreshExprSyntheticOpaqueMVar target tag
+let rfl    := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e
+let val    := mkApp2 mvar' e rfl
+assignExprMVar mvarId val
+let mvarId' := mvar'.mvarId!
+(_, mvarId') ← Meta.introNP mvarId' 2
 pure [mvarId']
 
 private def evalGeneralizeWithEq (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
-liftMetaTactic $ fun mvarId => do
-  mvarId      ← Meta.generalize mvarId e x false;
-  mvarDecl    ← getMVarDecl mvarId;
+liftMetaTactic fun mvarId => do
+  let mvarId      ← Meta.generalize mvarId e x false
+  let mvarDecl    ← getMVarDecl mvarId
   match mvarDecl.type with
-  | Expr.forallE _ _ b _ => do
-    (_, mvarId) ← Meta.intro1P mvarId;
-    eType       ← inferType e;
-    u           ← Meta.getLevel eType;
-    let eq     := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);
-    let target := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq (b.liftLooseBVars 0 1);
+  | Expr.forallE _ _ b _ =>
+    let (_, mvarId) ← Meta.intro1P mvarId
+    let eType       ← inferType e
+    let u           ← Meta.getLevel eType
+    let eq          := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0)
+    let target      := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq (b.liftLooseBVars 0 1)
     evalGeneralizeFinalize mvarId e target
   | _ => throwError "unexpected type after generalize"
 
 -- If generalizing fails, fall back to not replacing anything
 private def evalGeneralizeFallback (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
-liftMetaTactic $ fun mvarId => do
-  eType       ← inferType e;
-  u           ← Meta.getLevel eType;
-  mvarType    ← Meta.getMVarType mvarId;
-  let eq     := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);
-  let target := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq mvarType;
+liftMetaTactic fun mvarId => do
+  let eType    ← inferType e
+  let u        ← Meta.getLevel eType
+  let mvarType ← Meta.getMVarType mvarId
+  let eq       := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0)
+  let target   := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq mvarType
   evalGeneralizeFinalize mvarId e target
 
 def evalGeneralizeAux (h? : Option Name) (e : Expr) (x : Name) : TacticM Unit :=
 match h? with
-| none   => liftMetaTactic $ fun mvarId => do
-  mvarId ← Meta.generalize mvarId e x false;
-  (_, mvarId) ← Meta.intro1P mvarId;
+| none   => liftMetaTactic fun mvarId => do
+  let mvarId ← Meta.generalize mvarId e x false
+  let (_, mvarId) ← Meta.intro1P mvarId
   pure [mvarId]
 | some h =>
   evalGeneralizeWithEq h e x <|> evalGeneralizeFallback h e x
 
 @[builtinTactic Lean.Parser.Tactic.generalize] def evalGeneralize : Tactic :=
 fun stx => do
-  let h? := getAuxHypothesisName stx;
-  let x  := getVarName stx;
-  e ← elabTerm (stx.getArg 2) none;
+  let h? := getAuxHypothesisName stx
+  let x  := getVarName stx
+  let e ← elabTerm (stx.getArg 2) none
   evalGeneralizeAux h? e x
 
-end Tactic
-end Elab
-end Lean
+end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
index ffd80097eb..693d297e62 100644
--- a/src/Lean/Elab/Tactic/Location.lean
+++ b/src/Lean/Elab/Tactic/Location.lean
@@ -3,9 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-namespace Lean
-namespace Elab
-namespace Tactic
+new_frontend
+namespace Lean.Elab.Tactic
 
 inductive Location
 | wildcard
@@ -22,15 +21,13 @@ def location         := parser! "at " >> (locationWildcard <|> locationTarget <|
 ```
 -/
 def expandLocation (stx : Syntax) : Location :=
-let arg := stx.getArg 1;
+let arg := stx.getArg 1
 if arg.getKind == `Lean.Parser.Tactic.locationWildcard then Location.wildcard
 else if arg.getKind == `Lean.Parser.Tactic.locationTarget then Location.target
-else Location.localDecls $ (arg.getArg 0).getArgs.map fun stx => stx.getId
+else Location.localDecls $ arg.getArg 0 $.getArgs.map fun stx => stx.getId
 
 def expandOptLocation (stx : Syntax) : Location :=
 if stx.isNone then Location.target
 else expandLocation $ stx.getArg 0
 
-end Tactic
-end Elab
-end Lean
+end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 6000c94197..5ccc1c5ad9 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -6,52 +6,48 @@ Authors: Leonardo de Moura
 import Lean.Elab.Match
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.Induction
+new_frontend
 
-namespace Lean
-namespace Elab
-namespace Tactic
+namespace Lean.Elab.Tactic
 
 structure AuxMatchTermState :=
 (nextIdx : Nat := 1)
 (cases   : Array Syntax := #[])
 
 private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
-let matchAlts := matchTac.getArg 4;
-let alts      := (matchAlts.getArg 1).getArgs;
-newAlts ← alts.mapSepElemsM fun alt => do {
-  let alt    := alt.updateKind `Lean.Parser.Term.matchAlt;
-  let holeOrTacticSeq := alt.getArg 2;
+let matchAlts := matchTac.getArg 4
+let alts      := matchAlts.getArg 1 $.getArgs
+let newAlts ← alts.mapSepElemsM fun alt => do
+  let alt    := alt.updateKind `Lean.Parser.Term.matchAlt
+  let holeOrTacticSeq := alt.getArg 2
   if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
     pure alt
-  else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then do
-    s ← get;
-    let holeName := mkIdentFrom holeOrTacticSeq (parentTag ++ (`match).appendIndexAfter s.nextIdx);
-    newHole ← `(?$holeName:ident);
-    modify fun s => { s with nextIdx := s.nextIdx + 1};
+  else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
+    let s ← get
+    let holeName := mkIdentFrom holeOrTacticSeq (parentTag ++ (`match).appendIndexAfter s.nextIdx)
+    let newHole ← `(?$holeName:ident)
+    modify fun s => { s with nextIdx := s.nextIdx + 1}
     pure $ alt.setArg 2 newHole
-  else withFreshMacroScope do
-    newHole ← `(?rhs);
-    let newHoleId := newHole.getArg 1;
-    newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq );
-    modify fun s => { s with cases := s.cases.push newCase };
+  else MonadQuotation.withFreshMacroScope do -- TODO: why do we need MonadQuotation here
+    let newHole ← `(?rhs)
+    let newHoleId := newHole.getArg 1
+    let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
+    modify fun s => { s with cases := s.cases.push newCase }
     pure $ alt.setArg 2 newHole
-};
-let result  := matchTac.updateKind `Lean.Parser.Term.match;
-let result  := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts));
+let result  := matchTac.updateKind `Lean.Parser.Term.«match»
+let result  := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts))
 pure result
 
 private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Syntax × Array Syntax) := do
-(matchTerm, s) ← (mkAuxiliaryMatchTermAux parentTag matchTac).run {};
+let (matchTerm, s) ← (mkAuxiliaryMatchTermAux parentTag matchTac).run {}
 pure (matchTerm, s.cases)
 
 @[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic :=
 fun stx => do
-  tag ← getMainTag;
-  (matchTerm, cases) ← liftMacroM $ mkAuxiliaryMatchTerm tag stx;
-  refineMatchTerm ← `(tactic| refine $matchTerm);
-  let stxNew := mkNullNode (#[refineMatchTerm] ++ cases);
+  let tag ← getMainTag
+  let (matchTerm, cases) ← liftMacroM $ mkAuxiliaryMatchTerm tag stx
+  let refineMatchTerm ← `(tactic| refine $matchTerm)
+  let stxNew := mkNullNode (#[refineMatchTerm] ++ cases)
   withMacroExpansion stx stxNew $ evalTactic stxNew
 
-end Tactic
-end Elab
-end Lean
+end Lean.Elab.Tactic