2 coq emacs modes

[Hendrik Tews <tews@os.inf.tu-dresden.de>]

Hi,

with Stephane sponsoring my Proof General package there are now
two emacs modes for Coq in Debian:

- the one from the Coq package installed by /etc/emacs/site-start.d/50coq.el
- the one from Proof General installed by
  /etc/emacs/site-start.d/50proofgeneral.el 

If both coq and proofgeneral are installed then the coq mode from
proofgeneral is used, because the files in site-start.d are
loaded in alphabetic order and 50proofgeneral.el adds its entries
later to auto-mode-alist.

I just wanted to bring this to your attention. Of course, we can
also discuss possible solutions:

1) leave the situation as is
  People not using Proof General will hopefully not install Proof
  General and therefore don't see the problem.

2) make a separate package for the emacs mode in Coq
  This way users are forced to make a decision. However, it is
  questionable if this is worth the effort, because nobody seems
  to use the coq-mode distributed with coq. coq-mode from
  Coq was completely broken in squeeze (#605024) and only people
  using Proof General noticed it, i.e., people either install coq
  allone and do not use emacs _or_ they install coq and Proof
  General. 

3) delete coq-mode from package coq

4) ask a debconf question when Proof General is installed

I am against option 4 but all of 1-3 are fine with me.


Bye,

Hendrik Tews