PG xml and Melpa

We've been developing a new version of Proof General that works with the Coq XML protocol, which was introduced in Coq 8.5. The main benefit of that protocol is that it allows asynchronous processing of proofs, which in many cases, speeds up the processing of proof scripts.

Until now, the only IDE that supported the XML protocol was CoqIDE, leaving Emacs users in the cold.

Our plan is to create a Melpa package for this new version of Proof General. Since the code has not been widely-tested, the code should be considered a beta. We'll make an announcement once the package is available.

Eventually, the existing Proof General will assume "legacy" status, though it will continue to be available.