Hi, > 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.
Indeed this could correlate with the emacs upgrade a while ago. Weird enough, it shows that error even when there is nothing to do: A "make" of the respective .vo files says they are up-to-date, and disabling the automatic compilation of dependent files works around the issue. I don't know how that makes sense. The current "upstream" ProofGeneral snapshot (150202) also has the same issue. However, after enabling concurrent compilation of dependent files, things are working - errors reported by Coq are shown in emacs. Again, I don't know how that makes sense. Kind regards, Ralf -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected]
