diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index ec695095b1..ba235199e3 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -547,7 +547,8 @@ 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) ".."
+def ellipsis       := leading_parser (withAnonymousAntiquot := false)
+  ".." >> notFollowedBy "." "`.` immediately after `..`"
 def argument       :=
   checkWsBefore "expected space" >>
   checkColGt "expected to be indented" >>
diff --git a/tests/lean/ellipsisProjIssue.lean b/tests/lean/ellipsisProjIssue.lean
new file mode 100644
index 0000000000..6312eefd60
--- /dev/null
+++ b/tests/lean/ellipsisProjIssue.lean
@@ -0,0 +1 @@
+#check Nat.add ...succ
diff --git a/tests/lean/ellipsisProjIssue.lean.expected.out b/tests/lean/ellipsisProjIssue.lean.expected.out
new file mode 100644
index 0000000000..faa0e25471
--- /dev/null
+++ b/tests/lean/ellipsisProjIssue.lean.expected.out
@@ -0,0 +1 @@
+ellipsisProjIssue.lean:1:17: error: unexpected `.` immediately after `..`