Custom Query (361 matches)

When I try to process the following with coq 8.3 beta, emacs freezes with 100% cpu. This doesn't happen with coq 8.2.

Require Import MSets.
Module NatSet := MSetList.Make Nat_as_DT.
Print NatSet.

Using the newest development version (or older versions) with Emacs 23.3 fails with the following error message during compiling the lisp files:

emacs --batch --no-site-file -q  -eval '(setq load-path (append (mapcar (lambda (d) (concat "/home/noschinl/opt/ProofGeneral-4.1pre110309/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego pgshell phox generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile contrib/mmm/mmm-mode.el 

In toplevel form:
contrib/mmm/mmm-mode.el:165:12:Error: `font-lock-beginning-of-syntax-function' is an obsolete variable (as of Emacs 23.3); use `syntax-begin-function' instead.
make[1]: *** [contrib/mmm/mmm-mode.elc] Fehler 1
make[1]: Leaving directory `/home/noschinl/opt/ProofGeneral-4.1pre110309'
make: *** [compile] Fehler 2

I keep getting "Replaced xyz occurrences" in the xemacs minibuffer after each PG interaction, where xyz depends on the length of the text. As Makarius said, we don't think it is a PG but an xemacs thing. But since you asked me to put it here... Clemens seems to be using the same setup but gets no such message. I started getting it after updating my MAC OS and my xemacs to [version 21.4.20; April 2007].

Tobias