I've been carrying the attached commit on my private branch for a while
now.  It may be an improvement, but I've forgotten the details.  I used
proof-general for a while when I was learning Coq, but have since
removed it because I found it annoying that GNOME Shell misidentified my
normal Emacs as being an instance of Proof General.

      Mark