> Or by those who designed Emacs with a flat namespace for features and
> library files...

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 have the impression, the Emacs
> mode distributed with Coq is rarely used, I would suggest that Coq
> changes the names of 'coq, 'coq-db and 'coq-syntax.  Or supresses the
> installation of these files with the default  "make install".

Another take on it is that the two teams should join their efforts.

ProofGeneral-devel mailing list

Reply via email to