Cool! Should we think about putting this in a dev branch or do you feel confident enough to let it go to master directly? People seem to sync with master quite often.
Best P. Le mar. 18 déc. 2018 à 15:50, Stefan Monnier <monn...@iro.umontreal.ca> a écrit : > > > 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 _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
