Custom Query (361 matches)

Byte-compilation of ProofGeneral 4.2 with the Emacs 24.2.90 pretest version fails in pg-response.el:

In toplevel form:
generic/pg-response.el:104:23:Error: `special-display-regexps' is an
obsolete variable (as of 24.3); use `display-buffer-alist' instead.

The devlopment version (BZR trunk) of Emacs can hang when PG Coq is used together with Emacs' auto fill minor mode. You can, for instance, reproduce the error in the following way:

1. Start Emacs without any initialization; emacs -q -nsl
2. Load PG initialization: M-x load-file <path-to-PG>/generic/proof-site.el
3. Open a *.v file.
4. Activate auto fill mode: M-x auto-fill-mode
5. Place the cursor _afer_ a comment with more than `fill-column' many characters.
6. Press <enter> -> Emacs hangs, and must be killed.

Remark 1: You do not get an error if auto filling happens _inside_ a comment.

Remark 2: Emacs 24.2.1 does not have this problem at all.

With a sufficiently large definition, as attached, Proof General never finishes advancing past it, and also can't retract until I send an interrupt or kill the Coq process.

I'm using Coq 8.4, emacs 24.1.1, and have tried both the stable and development releases of Proof General.

It works fine in coqide, or as coqtop -emacs < bug.v.