diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 0598cb401fbdd..ae74e8639802d 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -752,7 +752,7 @@ We use them to implement `macro_rules` and `elab_rules` def namedArgument := leading_parser (withAnonymousAntiquot := false) atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")" def ellipsis := leading_parser (withAnonymousAntiquot := false) - ".." >> notFollowedBy "." "`.` immediately after `..`" + ".." >> notFollowedBy (checkNoWsBefore >> ".") "`.` immediately after `..`" def argument := checkWsBefore "expected space" >> checkColGt "expected to be indented" >>