Timeline
Nov 15, 2011:
Nov 13, 2011:
- 9:27 PM Ticket #431 ("This subproof is complete" appears at bottom of goals) created by
- 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
- Consider the following Coq proof script: […] In coqtop, each …
- 5:51 PM Ticket #430 (Make "Set Ltac Debug" work) reopened by
- Consider the following proof script: […] When Proof General …
- 9:50 AM Ticket #429 (Coq should support *trace* buffer for idtac output) closed by
- 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
- 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
- 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
- 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
- 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
- fixed: Fixed now in version 12.2 of proof-shell.el (CVS head, today's …
Oct 5, 2011:
- 12:37 PM Ticket #138 (Can't insert text after locking a comment) reopened by
- I am still having the same issue in PG 4.1 (the latest CVS version) …
Oct 3, 2011:
Sep 30, 2011:
- 10:58 AM Ticket #427 (defpacustom and undo) closed by
- duplicate: Already noted in #419. For what it's worth, my opinion is that …
Sep 29, 2011:
- 2:58 PM Ticket #427 (defpacustom and undo) created by
- Hi, defpacustom settings are not preserved over undo, at least not …
Sep 27, 2011:
- 10:19 AM Ticket #426 (proof-user-options custom group partly broken) closed by
- fixed
- 10:18 AM Ticket #426 (proof-user-options custom group partly broken) created by
- displaying this customization group gives an error and a lot of …
Sep 19, 2011:
- 12:31 PM Ticket #425 (Consider simplifying span amalgamation to match prover undo behaviour) created by
- With more flexible undo behaviour (e.g. linear undo in Isabelle), we …
Sep 14, 2011:
- 8:19 PM Ticket #421 (proof-shell-exit raises an exception "Buffer foo.v has no process") closed by
- fixed: Fixed with solution 1. Hendrik
- 12:43 PM Ticket #422 (Support for entering ellipsis in electric terminator mode) closed by
- fixed: I've added a patch which allows you to use a numeric prefix just as …
- 12:31 PM Ticket #423 (List customisation variables use wrong widget) closed by
- fixed: Fixed, thanks for the patch.
- 12:16 PM Ticket #424 (proof-shell-exit does not follow standard emacs policy with query-exit.) closed by
- fixed: Have made suggested change. Thanks for pointing out inconsistency.
Sep 11, 2011:
- 5:00 PM Ticket #424 (proof-shell-exit does not follow standard emacs policy with query-exit.) created by
- Currently, when there is a running prover process and user, hitting …
- 3:59 PM Ticket #423 (List customisation variables use wrong widget) created by
- Customisation variables which take a list of strings like …
- 1:56 PM Ticket #422 (Support for entering ellipsis in electric terminator mode) created by
- When electric-terminator is on, it's unclear how to enter an ellipsis …
- 1:50 PM Ticket #296 (PG accepts garbage though Coq said "illegal begin of vernac") reopened by
- In Coq trunk, I believe periods are not treated as end-of-command …
- 1:48 PM Ticket #421 (proof-shell-exit raises an exception "Buffer foo.v has no process") created by
- Hello, here is how to reproduce the bug: open a coq file (say …
Note: See TracTimeline
for information about the timeline view.