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.

P.
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to