Hendrik Tews <[email protected]> writes: This is going to be a problem for those that want to use a manually installed Coq 8.4 with a Debian installation of Proof General. In Debian, manually installed stuff has precedence, so when proof-site requires 'coq, Emacs will actually load coq.el from the Coq installation.
I only found out yesterday, that the load-path management is severely broken in Debian (I would say), see bug #676424. So I am not going to change the load-path management of Proof General now and manual installs of Coq 8.4 are going to work as usual. Nevertheless, we should try to solve the feature name conflicts. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
