aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-06-18Add more declarationsDavid Aspinall
2002-06-18Test using proof-nesting-depth before calling ResetDavid Aspinall
2002-06-14Minor changes.Pierre Courtieu
2002-06-14Print and Check guess their argument from the region or the stringPierre Courtieu
near the point.
2002-06-13Disable count-undos function, just use find-and-forget.David Aspinall
2002-06-13A nil setting of proof-kill-goal-command forces use of proof-find-and-forget ↵David Aspinall
for all retraction.
2002-06-13DocsDavid Aspinall
2002-06-13Experiment with showing real prover output for aborted proofs.David Aspinall
2002-06-12Revised find-and-forget function, which also works for count-undos.David Aspinall
2002-06-12More test cases, summary of situation.David Aspinall
2002-06-12Second variant of next-span, without doubly nested loopDavid Aspinall
2002-06-12Improve imp of next-spanDavid Aspinall
2002-06-12Note of another bugDavid Aspinall
2002-06-12Test for find-and-forget using Back always instead of Reset.David Aspinall
2002-06-12Add test t4 for extra depth of nestingDavid Aspinall
2002-06-12Make hack for XEmacs 21.4 also work for later versionsDavid Aspinall
2002-06-12Changed the CHANGES file for Coq.Pierre Courtieu
2002-06-12Nested proofs in Coq are well backtracked! I used the new fieldPierre Courtieu
'nestedundos created by David. Will change the CHANGE file accordingly.
2002-06-12Adjust proof-nesting depth, add FIXME notes since not right yetDavid Aspinall
2002-06-12New files.David Aspinall
2002-06-12Add proof-nested-undo-regexp settingDavid Aspinall
2002-06-12Add nestedundos setting to span, and proof-nested-undo-regexp settingDavid Aspinall
2002-06-11Replace with example from PierreDavid Aspinall
2002-06-11Only match saves for prover that supports nested proofs (restores old ↵David Aspinall
behaviour for Isar). Isar goal/save regexps dont match up properly.
2002-06-11Not important.Pierre Courtieu
2002-06-11CHANGE is cleaner in the Coq part! Not important.Pierre Courtieu
2002-06-11Added changes in CHANGE about my new customization variablesPierre Courtieu
coq-user-backable-command etc.
2002-06-11Added the coq-user-... elisp customization variables to allow the userPierre Courtieu
to defclare new commands and tactics: must typically be customized in .emacs.
2002-06-11Remove proof-nested-goals-p settingDavid Aspinall
2002-06-11Improved proof-nesting-depth (not finished yet)David Aspinall
2002-06-11Fixed a bug of the new synchro code (coq-find-and-forget) inPierre Courtieu
coq.el. Now do not count Tactics and unsaved goal commands for "Back".
2002-06-11Add proof-nesting-depth, new implementation of span amalgamation in ↵David Aspinall
proof-done-advancing.
2002-06-11Set nested goals; include Lemma again in def of goal.David Aspinall
2002-06-11New files.David Aspinall
2002-06-08Mention not supporting E21David Aspinall
2002-06-08Updated.David Aspinall
2002-06-08Add install for isartagsDavid Aspinall
2002-06-08Updated.David Aspinall
2002-06-08Fix bug in string syntax in isar-strip-terminators: did this work correctly ↵David Aspinall
before?
2002-06-08Clean up span.el loading; make compat with bbdb.el in FSFDavid Aspinall
2002-06-08Clean up span.el loadingDavid Aspinall
2002-06-08Updated.David Aspinall
2002-06-08UpdatesDavid Aspinall
2002-06-08Remove duplicateDavid Aspinall
2002-06-08Add isartagsDavid Aspinall
2002-06-08Program [broken]David Aspinall
2002-06-08Update magicDavid Aspinall
2002-06-08Default to /usr/bin/perlDavid Aspinall
2002-06-08Note about removing dirsDavid Aspinall
2002-06-08Remove PGK mention, other obs projectsDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 11:01:08 +0000