Good news! The license conditions for Proof General will shortly be changed to the GPL. This relaxes the current conditions in several ways, in particular, allowing packaging and distribution of the code by others.
We plan to release version 3.4 of Proof General
next month. This update will have several significant improvements
(notably to the synchronization support for Coq), and also includes
fixes and updates for recent versions of (X)Emacs and various proof assistants.
Please, please, please do test the development release for us in the
meantime and report any difficulties,
to help make the next release of Proof General as
robust as possible. Thanks!