On Thu, Nov 29, 2018 at 11:16 AM Emilio Jesús Gallego Arias <e...@x80.org> wrote: > As of today, you have coq-serapi[1], which was specifically designed to > make interaction with Emacs easy.
That helps a bit for some issues, but I think most of the bugs in the async branch mostly relate to maintaining unstated or unknown invariants in the implementation. > Also, a LSP server for Coq is expected to appear very soon. That would be a definite advance for all IDEs. -- Paul _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel