The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I have noticed that there are some minor interaction problems between 
Coq and Proof General, and am wondering if other users have similar 
issues - and if so, if they have workarounds.

One is that Proof General no longer keeps the Goals window updated with 
respect to undo and backwards goto steps - it is usually just cleared, 
but it can sometimes show a former goal state.  I don't recall when this 
stopped working, but I do think Coq and Proof General once did keep the 
Goals window perfectly in sync with all undo and goto steps.  ^C-^P 
still works to display the current proof state, but I now have to use it 
excessively.

Another nuisance is that some responses never appear - for instance Time 
and info_eauto output in certain cases (not all, but most) never shows 
up in the response window.  Or, maybe it does but gets immediately 
cleared.  Again, I think this used to work.

I'm using a recent trunk version of Coq with the most recent version of 
Proof General (4.3pre131011).

Thanks in advance for any assistance.
-- Jonathan