Bad syntax error recovery

[thery]

I am with vscoq 2.2.5 coq 8.20.1

Ok I have a file with an obvious syntax error. Anyway I try to execute it anyway (this is important)

now if I try to correct the error, the error message remains shitted of some characters.

If I don't try to execute the line with a syntax error, correcting works fine.

[gares]

@rtetley do you promote the parse error to an exec one when one executes a not-parsed sentece?

[rtetley]

I believe I do

[thery]

can you reproduce the error?

[rtetley]

I can reproduce it indeed. However the error that is produced after correcting is not the same ! So I don't believe it's a shift, the system detects a new parse error... I don't know why yet though...