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

Reply via email to