Opened 13 years ago
Last modified 9 years ago
#429 reopened enhancement
Should give output of multiple idtac invocations — at Initial Version
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | ezyang@… |
Description
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.
Note: See
TracTickets for help on using
tickets.
