Custom Query (361 matches)

See the test case in coq/ex/test-cases/change-ancestor/README.

The problem appears when one asserts text that has just been added at the end of an completely locked ancestor. Then Proof General sends only the newly added portion to Coq instead of the complete buffer.

cd doc; make dvi therefore gives

make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" dvi make[1]: Entering directory `/home/tews/src/pg/doc' make[1]: * No rule to make target `dvi'. Stop. make[1]: Leaving directory `/home/tews/src/pg/doc' make: * [dvi] Error 2

If the dvi format is not supported any more I suggest to remove all occurrences of dvi from doc/Makefile and doc/Makefile.doc.

Hendrik

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