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

fix: sepBy

Browse source 
If parser consumed something, keep error.
This commit is contained in:
Leonardo de Moura 2020-02-21 11:43:45 -08:00
parent 9694102b3e
commit bb0bfb5742
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Lean/Parser/Parser.lean
View file

@ -444,7 +444,8 @@ fun c s =>
let pos := s.pos;
let s := p c s;
if s.hasError then
if pOpt then
if s.pos > pos then s
else if pOpt then
let s := s.restore sz pos;
if s.stackSize - iniSz == 2 && unboxSingleton then
s.popSyntax