I’m having an issue - it looks like a bug, but I don’t know what the proper reporting procedure is or how to express a minimal example so I’m hoping for some advice here.
I can use C^c RET to move the proof buffer past its current point, but not back to a previous point. C^c C^r doesn’t work either. When I do these, i get one of two different errors:
Error: the reference Backtrack was not found in the current environment
Error: Syntax error illegal begin of toplevel:vernac_toplevel
Also, my cursor jumps forward to the first line of code after the end of the proof buffer
I think i updated coq and proof general. I dont know if there are other things i have to update? also I can’t find anything about these errors on google