> 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 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.
Stefan
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
