chore: update stage0

stage0/src/Lean/Elab/Do.lean

@@ -127,10 +127,10 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn
         rest ← mkRest ();
         newBody ←
           if optElse.isNone then do
-            `(do let x ← $discr; match x with | $pat => $rest)
+            `(do let x ← $discr; (match x with | $pat => $rest))
           else
             let elseBody := optElse.getArg 1;
-            `(do let x ← $discr; match x with | $pat => $rest | _ => $elseBody);
+            `(do let x ← $discr; (match x with | $pat => $rest | _ => $elseBody));
         addPrefix newBody
       else if i < doElems.size - 1 && doElem.getKind == `Lean.Parser.Term.doExpr then do
         -- def doExpr := parser! termParser

stage0/src/Lean/Parser/Do.lean

@@ -131,7 +131,13 @@ def doMatchAlts : Parser := parser! withPosition fun pos => (optional "| ") >> s
 @[builtinDoElemParser] def «break» := parser! "break"
 @[builtinDoElemParser] def «continue» := parser! "continue"
 
-@[builtinDoElemParser] def doExpr   := parser! notFollowedBy "let " >> notFollowedBy "have " >> termParser
+/-
+We use `notFollowedBy` to avoid counterintuitive behavior. For example, the `if`-term parser
+doesn't enforce indentation restrictions, but we don't want it to be used when `doIf` fails.
+Note that parser priorities would not solve this problem since the `doIf` parser is failing while the `if`
+parser is succeeding.
+-/
+@[builtinDoElemParser] def doExpr   := parser! notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do") >> termParser
 
 @[builtinTermParser] def «do»  := parser!:maxPrec "do " >> doSeq