aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-06-19Doc improvementsDavid Aspinall
2002-06-19Finished updating the commands and tactic lists of coq-syntax.el.Pierre Courtieu
2002-06-19updated the lists of commands and tactics in coq-syntax.el.Pierre Courtieu
2002-06-19Use coq-proof-mode-p instead of nesting depth test. Attempt to track ↵David Aspinall
nesting depth (fails).
2002-06-19Add nested section example to increase the horror.David Aspinall
2002-06-19Added End for sections, and silly testDavid Aspinall
2002-06-19Updated with more notesDavid Aspinall
2002-06-19Clean up: remove count-undos, comments, tweak coq-proof-mode-p.David Aspinall
2002-06-19Updated.David Aspinall
2002-06-19Add proof-shell-last-prompt.David Aspinall
2002-06-19Add doc of proof-shell-last-prompt.David Aspinall
2002-06-19Fix infoDavid Aspinall
2002-06-19Set version tag for new release.David Aspinall
2002-06-18Update Emacs versionsDavid Aspinall
2002-06-18Add news for PG 3.4David Aspinall
2002-06-18Update magic. Document nested proof settings.David Aspinall
2002-06-18Removed lift-global stuff. coq-find-and-forget: only undo undoable tactics.David Aspinall
2002-06-18Remove lift-global function.David Aspinall
2002-06-18Remove global testing and lift-global function; rename proof-nested-goals -> ↵David Aspinall
proof-nested-goals-history.
2002-06-18Added some non-undoable tacticsDavid Aspinall
2002-06-18Added some sectionsDavid Aspinall
2002-06-18News item for PG 3.4David Aspinall
2002-06-18Added the backtrack mechanism for sections. Seems to work.Pierre Courtieu
2002-06-18Added a function to inspect the prompt of Coq, in order to know if wePierre Courtieu
are in proof-mode. Redundant with proof-nesting-depth.
2002-06-18Attempt at (alledgedly) more robust solution to find-and-forget.David Aspinall
2002-06-18FixDavid Aspinall
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 23:16:53 +0000