Hi, sorry for the false alarm, the problem is in file /usr/share/emacs/site-lisp/coq/coq.el from package coq, which requires hilit19, See #605024.
The problem with proofgeneral is, that it does not install its on bindings for *.v files on startup. Therefore one hits coq-mode from package coq, even when proofgeneral is installed. It would help if proofgeneral would override the broken coq bindings on emacs startup. Workaround: put (proofgeneral) in your .emacs or do M-x proofgeneral before loading a .v file. Bye, Hendrik -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]

