aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Add proof-shell-last-prompt.Gravatar David Aspinall2002-06-19
|
* Add doc of proof-shell-last-prompt.Gravatar David Aspinall2002-06-19
|
* Fix infoGravatar David Aspinall2002-06-19
|
* Set version tag for new release.Gravatar David Aspinall2002-06-19
|
* Update Emacs versionsGravatar David Aspinall2002-06-18
|
* Add news for PG 3.4Gravatar David Aspinall2002-06-18
|
* Update magic. Document nested proof settings.Gravatar David Aspinall2002-06-18
|
* Removed lift-global stuff. coq-find-and-forget: only undo undoable tactics.Gravatar David Aspinall2002-06-18
|
* Remove lift-global function.Gravatar David Aspinall2002-06-18
|
* Remove global testing and lift-global function; rename proof-nested-goals -> ↵Gravatar David Aspinall2002-06-18
| | | | proof-nested-goals-history.
* Added some non-undoable tacticsGravatar David Aspinall2002-06-18
|
* Added some sectionsGravatar David Aspinall2002-06-18
|
* News item for PG 3.4Gravatar David Aspinall2002-06-18
|
* Added the backtrack mechanism for sections. Seems to work.Gravatar Pierre Courtieu2002-06-18
|
* Added a function to inspect the prompt of Coq, in order to know if weGravatar Pierre Courtieu2002-06-18
| | | | are in proof-mode. Redundant with proof-nesting-depth.
* Attempt at (alledgedly) more robust solution to find-and-forget.Gravatar David Aspinall2002-06-18
|
* FixGravatar David Aspinall2002-06-18
|
* Add more declarationsGravatar David Aspinall2002-06-18
|
* Test using proof-nesting-depth before calling ResetGravatar David Aspinall2002-06-18
|
* Minor changes.Gravatar Pierre Courtieu2002-06-14
|
* Print and Check guess their argument from the region or the stringGravatar Pierre Courtieu2002-06-14
| | | | near the point.
* Disable count-undos function, just use find-and-forget.Gravatar David Aspinall2002-06-13
|
* A nil setting of proof-kill-goal-command forces use of proof-find-and-forget ↵Gravatar David Aspinall2002-06-13
| | | | for all retraction.
* DocsGravatar David Aspinall2002-06-13
|
* Experiment with showing real prover output for aborted proofs.Gravatar David Aspinall2002-06-13
|
* Revised find-and-forget function, which also works for count-undos.Gravatar David Aspinall2002-06-12
|
* More test cases, summary of situation.Gravatar David Aspinall2002-06-12
|
* Second variant of next-span, without doubly nested loopGravatar David Aspinall2002-06-12
|
* Improve imp of next-spanGravatar David Aspinall2002-06-12
|
* Note of another bugGravatar David Aspinall2002-06-12
|
* Test for find-and-forget using Back always instead of Reset.Gravatar David Aspinall2002-06-12
|
* Add test t4 for extra depth of nestingGravatar David Aspinall2002-06-12
|
* Make hack for XEmacs 21.4 also work for later versionsGravatar David Aspinall2002-06-12
|
* Changed the CHANGES file for Coq.Gravatar Pierre Courtieu2002-06-12
|
* Nested proofs in Coq are well backtracked! I used the new fieldGravatar Pierre Courtieu2002-06-12
| | | | | 'nestedundos created by David. Will change the CHANGE file accordingly.
* Adjust proof-nesting depth, add FIXME notes since not right yetGravatar David Aspinall2002-06-12
|
* New files.Gravatar David Aspinall2002-06-12
|
* Add proof-nested-undo-regexp settingGravatar David Aspinall2002-06-12
|
* Add nestedundos setting to span, and proof-nested-undo-regexp settingGravatar David Aspinall2002-06-12
|
* Replace with example from PierreGravatar David Aspinall2002-06-11
|
* Only match saves for prover that supports nested proofs (restores old ↵Gravatar David Aspinall2002-06-11
| | | | behaviour for Isar). Isar goal/save regexps dont match up properly.
* Not important.Gravatar Pierre Courtieu2002-06-11
|
* CHANGE is cleaner in the Coq part! Not important.Gravatar Pierre Courtieu2002-06-11
|
* Added changes in CHANGE about my new customization variablesGravatar Pierre Courtieu2002-06-11
| | | | coq-user-backable-command etc.
* Added the coq-user-... elisp customization variables to allow the userGravatar Pierre Courtieu2002-06-11
| | | | | to defclare new commands and tactics: must typically be customized in .emacs.
* Remove proof-nested-goals-p settingGravatar David Aspinall2002-06-11
|
* Improved proof-nesting-depth (not finished yet)Gravatar David Aspinall2002-06-11
|
* Fixed a bug of the new synchro code (coq-find-and-forget) inGravatar Pierre Courtieu2002-06-11
| | | | coq.el. Now do not count Tactics and unsaved goal commands for "Back".
* Add proof-nesting-depth, new implementation of span amalgamation in ↵Gravatar David Aspinall2002-06-11
| | | | proof-done-advancing.
* Set nested goals; include Lemma again in def of goal.Gravatar David Aspinall2002-06-11
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 02:19:03 +0000