> Thanks Stefan for all this cleanup! You're welcome. Here comes something more substantial. The patch below (along with a few more not-directly-related tweaks) makes a fairly significant internal change to try and pry apart coq-mode and PG. The main part is that `coq-mode` is now a normal major mode, which we enter directly (rather than going through a stub generated by proof-site.el) and which can optionally use ProofGeneral (controlled by `coq-use-pg` which of course defaults to t).
The internal dependencies are still not completely fixed, tho: loading
coq-mode.el still ends up loading a lot of PG code as well (IOW, the fun
isn't over yet).
Stefan
0001-coq-mode.el-New-file-to-make-coq-mode-independent-fr.patch
Description: Binary data
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
