#109 closed defect (fixed)
Missing output from Coq
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-3.7 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
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" )
Change History (2)
comment:1 Changed 17 years ago by
comment:2 Changed 17 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
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).
Note: See
TracTickets for help on using
tickets.
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
(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