Timeline



Jan 10, 2012:

5:33 PM Ticket #433 (unexpected cursor position after stepping through command with ...) created by coquser
Disclaimer: I am fairly new with PG and not yet used to the …
1:15 PM Ticket #430 (Make "Set Ltac Debug" work) closed by David Aspinall
fixed: The UI will now switch to display the *coq* window when debugging. …
11:54 AM Ticket #432 (Add documentation of *trace* buffer to PG Adapting manual) closed by David Aspinall
fixed
11:41 AM Ticket #429 (Coq should support *trace* buffer for idtac output) closed by David Aspinall
upstream: Waiting until Coq developers take note or someone supplies a patch to …
11:37 AM Ticket #378 (Makefile "make" should detect wrong bytecode file version and rebuild) closed by David Aspinall
wontfix: Giving up on this in absence of any proposed patch. Many software …

Jan 9, 2012:

3:29 PM Ticket #431 ("This subproof is complete" appears at bottom of goals) closed by David Aspinall
needmoreinfo: Could you upload a simple example please? (So non Coq user may try)

Dec 17, 2011:

9:17 AM WikiStart edited by David Aspinall
(diff)

Dec 7, 2011:

3:29 PM Ticket #428 (subsubsection links not working in PG doc) closed by coquser
fixed: The problem was in the php parsing of the doc files, which was not …

Nov 15, 2011:

12:58 PM Ticket #432 (Add documentation of *trace* buffer to PG Adapting manual) created by David Aspinall

Nov 13, 2011:

9:27 PM Ticket #431 ("This subproof is complete" appears at bottom of goals) created by Robin Green
After a bulleted subproof has been completed, […] appears at the …

Nov 9, 2011:

6:20 PM Ticket #429 (Coq should support *trace* buffer for idtac output) reopened by coquser
Consider the following Coq proof script: […] In coqtop, each …
5:51 PM Ticket #430 (Make "Set Ltac Debug" work) reopened by coquser
Consider the following proof script: […] When Proof General …
9:50 AM Ticket #429 (Coq should support *trace* buffer for idtac output) closed by David Aspinall
needmoreinfo: It sounds like this would be useful, could you give a bit more …
9:48 AM Ticket #430 (Make "Set Ltac Debug" work) closed by David Aspinall
invalid: Could you give a bit more of a description of what you want to be …

Nov 7, 2011:

5:14 AM Ticket #430 (Make "Set Ltac Debug" work) created by coquser
When Proof General attempts to handle compound tactics in debug mode, …
5:13 AM Ticket #429 (Coq should support *trace* buffer for idtac output) created by coquser
When debugging proof search, it's often useful to use idtac for printf …

Oct 24, 2011:

10:20 AM Ticket #428 (subsubsection links not working in PG doc) created by coquser
Hi, in the Proof General documentation at …

Oct 17, 2011:

12:16 PM Ticket #138 (Can't insert text after locking a comment) closed by David Aspinall
fixed: Fixed now in version 12.2 of proof-shell.el (CVS head, today's …
Note: See TracTimeline for information about the timeline view.