Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Coq with Proof general questions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq with Proof general questions


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page