The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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