2012/6/6 Stefan Monnier <monn...@iro.umontreal.ca>:
> Another take on it is that the two teams should join their efforts.

I already asked why this old file is still in coq distribution. The
answer was: some people just want to open coq file for syntax
highlighting. For them starting pg is too slow (+ splash screen).

I am ready to convince coq people to remove them if we can provide
some switch for a "light" PG loading where no scripting feature is
provided. In this case we could simply ask that that no emacs file
should be distributed with coq.

ProofGeneral-devel mailing list

Reply via email to