Missing output from Coq

[David Aspinall]

Dear Proof General developers,

In Coq, the identity tactic, idtac, is also used to print its arguments, for example, for debugging purposes. However, I don't see the output of idtac either in the *goals* or in the *response* buffer.

For example, I don't see any output after executing the following script:

Goal True.
idtac "Hello!".

Is there a way to correct this?

Thank you, Yeveniy Makarov

Emacs  : GNU Emacs 21.4.1 (i386-redhat-linux-gnu, X toolkit, Xaw3d scroll bars)
 of 2006-03-07 on hs20-bc1-6.build.redhat.com
Package: Proof General

current state:
==============
(setq
 proof-general-version "Proof General Version 3.6pre061027. Released by da."
 proof-assistant "Coq"
 )

[David Aspinall]

PS I don't think you mentioned which Coq version you're using, which could be important.

That's right. It's Trunk Revision: 9700, one of the very latest snapshots at Coq repository ​svn://scm.gforge.inria.fr/svn/coq/trunk. It can be checked out using the command

svn checkout svn://scm.gforge.inria.fr/svn/coq

(see also ​http://gforge.inria.fr/scm/?group_id=269)

This revision is past Coq version 8.1, which was released recently.

Thank you, Yevgeniy

[courtieu]

OK, this should be fixed. When Coq outputs a message followed by the goals, it should display both now.

To developers: we need something generic to do that (if the output matches goal regexp, we should go on treating what was not matched).