diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 11387a1d9d..1f0b2587e9 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -42,7 +42,7 @@ match expectedType? with private def getDoElems (stx : Syntax) : Array Syntax := let arg := stx.getArg 1; -if arg.getKind == `Lean.Parser.Term.doSeqBracketed || arg.getKind == `Lean.Parser.Term.bracketedDoSeq /- TODO: remove second case -/ then +if arg.getKind == `Lean.Parser.Term.doSeqBracketed then (arg.getArg 1).getArgs else arg.getArgs