Changes between Initial Version and Version 1 of Ticket #429


Ignore:
Timestamp:
Nov 9, 2011, 9:50:11 AM (12 years ago)
Author:
David Aspinall
Comment:

It sounds like this would be useful, could you give a bit more description and example please so a non-Coq user can understand? Also, please add more info to #430 if that's a different case.

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #429

    • Property Status changed from new to closed
    • Property Resolution changed from to needmoreinfo

  • Ticket #429 – Description

    initial v1  
    1 When debugging proof search, it's often useful to use idtac for printf debugging. Unfortunately, we can't do this in ProofGeneral, because it only gives us the last idtac output. It would be really nice if ProofGeneral worked more like coqtop in this respect.
     1When debugging proof search, it's often useful to use idtac for printf debugging. Unfortunately, we can't do this in !ProofGeneral, because it only gives us the last idtac output. It would be really nice if !ProofGeneral worked more like coqtop in this respect.