The Coq mailing list

[Joey Dodds <jdodds AT princeton.edu>]

One workaround for the printing of Time and friends is that you can find the output in the *coq* buffer.

Joey

On Mon, Jun 16, 2014 at 11:25 AM, Jonathan <jonikelee AT gmail.com> wrote:

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