Evaluation highlight can sometimes become desynced from text

[varkor]

I haven't figured out a way to consistently reproduce this yet, but sometimes Step backwards, etc. can start selecting text that doesn't represent the actual steps, meaning the highlighted text is desynced from the proof state. I think sometimes it occurs when pasting text into the program.

[varkor]

I'm not sure if this is the same issue, but sometimes only closing the window and reopening it will fix a Coq error — even Coq: Reset does not suffice.