The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Jonathan,

Indeed pg is a bit out of sync with coq trunk currently.

I am trying to save some time to fix it. I aim at maintaining the same kind of features as for coq 8.4. Understand: I don't have enough time to implement something using asynchronous protocol for now. Maybe later if other emerging interfaces do not grow mature enough.

Best regards,

Pierre

Le Sat Dec 13 2014 at 5:27:27 PM, Jonathan <jonikelee AT gmail.com> a écrit :

For a while now I've been flipping back and forth between using PG and
CoqIDE, mostly because for some reason PG no longer shows idtac messages
(and other non-failure messages, such as from the Time command) in most
cases.  It only shows them when the message-producing tactic also solves
the goal.

I'm wondering if anyone else has this issue with idtac in PG, or if I
somehow have it misconfigured.

I'm using a recent trunk version of Coq and the most recent development
version of PG (which is more than a year old).

-- Jonathan