coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Coq with Proof general questions
- Date: Mon, 16 Jun 2014 14:25:51 -0400
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
- [Coq-Club] Coq with Proof general questions, Jonathan, 06/16/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] Coq with Proof general questions, Joey Dodds, 06/16/2014
Archive powered by MHonArc 2.6.18.