max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-26 13:39:55 -07:00
parent 8a06b04f3a
commit 17e97baf8d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Do.lean
View file

@ -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