Hendrik Tews <t...@os.inf.tu-dresden.de> writes:

   Regarding the 4.3 release: ...

I have another issue that I would like to see resolved in 4.3:
The feature name conflict with Coq, see

Both Proof General and Coq install coq.el (and some other files
with identical name), which cases trouble, because the feature
name space of Emacs is flat.

Possible solutions (with decreasing preference for me) are:

- The defending files are deleted in Coq or are not installed by
  the default make install.

- The files are renamed in the Coq distribution.

- The files are renamed in Proof General.


ProofGeneral-devel mailing list

Reply via email to