Re: 2 coq emacs modes

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

David MENTRE writes:
   
   Another proposal:
   
     5) Still install coq-mode but request a user action (i.e. putting
   something in .emacs) to activate it. Document it in README.Debian.
   
Indeed, this was the way the old Proof General package handled
the situation. It lead to quite a bit of confusion, see bugs
#582768, #605014, #605024. 

When people install an Emacs package in Debian they expect it to
work after restarting Emacs. Therefore, I would not like to see
5) for the coq-mode of Proof General. For the coq-mode of coq 5)
would be fine with me, because IMHO nobody is using it, at least
not the one distributed with Debian.

Bye,

Hendrik