Hello, 2012/1/13 Hendrik Tews <tews@os.inf.tu-dresden.de>: > 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. Yes, yhis was the intent of my proposal: explicit activation for coq-mode of Coq, implicit activation for ProofGeneral's coq-mode. Best regards, d.