Thanks for reporting this. I remember having problems with this when I originally wrote the compilation feature for Coq. IIRC, the problem is that there is no clear interface for inserting text in write protected buffers. Probably the hack that I used for this broke in the newest emacs version. I have to check this.
Bye, Hendrik -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected]
