| Age | Commit message (Expand) | Author |
| 2002-06-19 | Use coq-proof-mode-p instead of nesting depth test. Attempt to track nesting... | David Aspinall |
| 2002-06-19 | Add nested section example to increase the horror. | David Aspinall |
| 2002-06-19 | Added End for sections, and silly test | David Aspinall |
| 2002-06-19 | Updated with more notes | David Aspinall |
| 2002-06-19 | Clean up: remove count-undos, comments, tweak coq-proof-mode-p. | David Aspinall |
| 2002-06-19 | Updated. | David Aspinall |
| 2002-06-19 | Add proof-shell-last-prompt. | David Aspinall |
| 2002-06-19 | Add doc of proof-shell-last-prompt. | David Aspinall |
| 2002-06-19 | Fix info | David Aspinall |
| 2002-06-19 | Set version tag for new release. | David Aspinall |
| 2002-06-18 | Update Emacs versions | David Aspinall |
| 2002-06-18 | Add news for PG 3.4 | David Aspinall |
| 2002-06-18 | Update magic. Document nested proof settings. | David Aspinall |
| 2002-06-18 | Removed lift-global stuff. coq-find-and-forget: only undo undoable tactics. | David Aspinall |
| 2002-06-18 | Remove lift-global function. | David Aspinall |
| 2002-06-18 | Remove global testing and lift-global function; rename proof-nested-goals -> ... | David Aspinall |
| 2002-06-18 | Added some non-undoable tactics | David Aspinall |
| 2002-06-18 | Added some sections | David Aspinall |
| 2002-06-18 | News item for PG 3.4 | David Aspinall |
| 2002-06-18 | Added the backtrack mechanism for sections. Seems to work. | Pierre Courtieu |
| 2002-06-18 | Added a function to inspect the prompt of Coq, in order to know if we | Pierre Courtieu |
| 2002-06-18 | Attempt at (alledgedly) more robust solution to find-and-forget. | David Aspinall |
| 2002-06-18 | Fix | David Aspinall |
| 2002-06-18 | Add more declarations | David Aspinall |
| 2002-06-18 | Test using proof-nesting-depth before calling Reset | David Aspinall |
| 2002-06-14 | Minor changes. | Pierre Courtieu |
| 2002-06-14 | Print and Check guess their argument from the region or the string | Pierre Courtieu |
| 2002-06-13 | Disable count-undos function, just use find-and-forget. | David Aspinall |
| 2002-06-13 | A nil setting of proof-kill-goal-command forces use of proof-find-and-forget ... | David Aspinall |
| 2002-06-13 | Docs | David Aspinall |
| 2002-06-13 | Experiment with showing real prover output for aborted proofs. | David Aspinall |
| 2002-06-12 | Revised find-and-forget function, which also works for count-undos. | David Aspinall |
| 2002-06-12 | More test cases, summary of situation. | David Aspinall |
| 2002-06-12 | Second variant of next-span, without doubly nested loop | David Aspinall |
| 2002-06-12 | Improve imp of next-span | David Aspinall |
| 2002-06-12 | Note of another bug | David Aspinall |
| 2002-06-12 | Test for find-and-forget using Back always instead of Reset. | David Aspinall |
| 2002-06-12 | Add test t4 for extra depth of nesting | David Aspinall |
| 2002-06-12 | Make hack for XEmacs 21.4 also work for later versions | David Aspinall |
| 2002-06-12 | Changed the CHANGES file for Coq. | Pierre Courtieu |
| 2002-06-12 | Nested proofs in Coq are well backtracked! I used the new field | Pierre Courtieu |
| 2002-06-12 | Adjust proof-nesting depth, add FIXME notes since not right yet | David Aspinall |
| 2002-06-12 | New files. | David Aspinall |
| 2002-06-12 | Add proof-nested-undo-regexp setting | David Aspinall |
| 2002-06-12 | Add nestedundos setting to span, and proof-nested-undo-regexp setting | David Aspinall |
| 2002-06-11 | Replace with example from Pierre | David Aspinall |
| 2002-06-11 | Only match saves for prover that supports nested proofs (restores old behavio... | David Aspinall |
| 2002-06-11 | Not important. | Pierre Courtieu |
| 2002-06-11 | CHANGE is cleaner in the Coq part! Not important. | Pierre Courtieu |
| 2002-06-11 | Added changes in CHANGE about my new customization variables | Pierre Courtieu |