aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* 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
* 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
* 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
* 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 behavio...Gravatar David Aspinall2002-06-11
* 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
* Added the coq-user-... elisp customization variables to allow the userGravatar Pierre Courtieu2002-06-11
* 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
* Add proof-nesting-depth, new implementation of span amalgamation in proof-don...Gravatar David Aspinall2002-06-11
* Set nested goals; include Lemma again in def of goal.Gravatar David Aspinall2002-06-11
* New files.Gravatar David Aspinall2002-06-11
* Mention not supporting E21Gravatar David Aspinall2002-06-08
* Updated.Gravatar David Aspinall2002-06-08
* Add install for isartagsGravatar David Aspinall2002-06-08
* Updated.Gravatar David Aspinall2002-06-08
* Fix bug in string syntax in isar-strip-terminators: did this work correctly b...Gravatar David Aspinall2002-06-08
* Clean up span.el loading; make compat with bbdb.el in FSFGravatar David Aspinall2002-06-08
* Clean up span.el loadingGravatar David Aspinall2002-06-08
* Updated.Gravatar David Aspinall2002-06-08
* UpdatesGravatar David Aspinall2002-06-08
* Remove duplicateGravatar David Aspinall2002-06-08