Hendrik Tews <t...@os.inf.tu-dresden.de> 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.
ProofGeneral-devel mailing list