#429 reopened enhancement (needmoreinfo)
Should give output of multiple idtac invocations — at Version 1
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | ezyang@… |
Description (last modified by )
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.
Change History (1)
comment:1 Changed 13 years ago by
| Description: | modified (diff) |
|---|---|
| Resolution: | → needmoreinfo |
| Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
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.