Hendrik Tews <hend...@askra.de> writes: > > (Yes, Coq and Proof General should not use the same Emacs feature > name for different packages.
Oh, I see they're not really different, just the coq one is smaller and maybe older. For the debian packages I'd suggest proofgeneral could supercede the coq one, either forcibly move it downward in the load-path, or perhaps the order would be right anyway if the coq package uses debian-pkg-add-load-path-item -- which it ought to do anyway. > http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2012/000241.html) The mixture of debian proofgeneral and manually installed coq or vice-versa which you mention is probably best left to the sysadmin. I'd think anything in /usr/local ought to have precedence. If the sysadmin has put something which doesn't work then it's not a debian package fault :-). -- To UNSUBSCRIBE, email to debian-bugs-rc-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org