[PG-devel] Feature name conflict with Coq

2012-06-06 Thread Hendrik Tews
Hi, both Proof General and Coq install and provide Emacs files and features for 'coq, 'coq-db and 'coq-syntax (the latter two are actually old versions from Proof General). 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

Re: [PG-devel] Feature name conflict with Coq

2012-06-06 Thread Stefan Monnier
Or by those who designed Emacs with a flat namespace for features and library files... Ahem! Please don't put .../ProofGeneral/coq in the load-path, and then simply do (require 'coq/coq). However, I believe it would be better if Coq and Proof General use different feature names. Because I