| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1997-10-22 | Updated proof-segment-up-to to take ""'s into account | Healfdene Goguen | |
| Hence, << Cd "../x". >> works in Coq, and << echo "hello; world"; >> should work in LEGO But maybe we don't want "Cd"'s at all... | |||
| 1997-10-17 | proof-active-terminator inside comment case fixed. Also maybe the | Dilip Sequiera | |
| continuous pbp-buffer update bug. | |||
| 1997-10-17 | Fixed coq-shell-prompt-pattern to reflect proof-id | Healfdene Goguen | |
| Changed ";" to "." in coq-save-with-hole-regexp New modifications to syntax table to reflect actual use of symbols in Coq | |||
| 1997-10-17 | Added "Induction" as tactic | Healfdene Goguen | |
| 1997-10-17 | fixed a bug in proof-process-active-terminator. Notice that it still | Thomas Kleymann | |
| doesn't work when you are inside a comment and press the proof-terminal-char | |||
| 1997-10-16 | Figured out display tables. | Dilip Sequiera | |
| 1997-10-16 | Merged Coq changes with main branch. | Dilip Sequiera | |
| 1997-10-16 | Merged Coq changes onto main branch | Dilip Sequiera | |
| 1997-10-16 | merged script management (1.10.2.18) with main branch | Thomas Kleymann | |
| 1997-10-16 | o merged script management (1.20.2.11) on the main branch | Thomas Kleymann | |
| o fixed a bug in lego-find-and-forget due to new treatment of comments | |||
| 1997-10-14 | proof-process-active-terminator is now an extension of | Thomas Kleymann | |
| proof-assert-until-point (it was broken and looks healthier now) | |||
| 1997-10-13 | *** empty log message *** | Thomas Kleymann | |
| 1997-10-13 | put script-management branch back on main branch | Thomas Kleymann | |
| 1997-10-13 | The package pbp is now integrated in the proof package | Thomas Kleymann | |
| 1997-10-13 | lego-count-undos is now aware that comments are treated separately | Thomas Kleymann | |
| 1997-10-08 | *** empty log message *** | Healfdene Goguen | |
| 1997-09-18 | X-Symbol version 4.45 beta | David Aspinall | |
| 1997-09-18 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1997-09-17 | X-Symbol version 4.45 beta | David Aspinall | |
| 1997-09-17 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1997-08-25 | minor change in font-lock pattern | Thomas Kleymann | |
| 1997-03-06 | implementation of pbptop now records if selected goal is not current, | Thomas Kleymann | |
| hence pbp-construct-command does not need to bother to cater for "Next" command | |||
| 1997-01-27 | improved highlighting of error messages | Thomas Kleymann | |
| 1996-12-12 | support for highlighting Error messages in pbp-mode without using font-lock | Thomas Kleymann | |
| 1996-12-12 | removed font-lock support for Error messages; this is now supported in | Thomas Kleymann | |
| the pbp package | |||
| 1996-12-09 | Took out some debugging code accidentally left in. | Dilip Sequiera | |
| 1996-12-09 | Speeded up proof-by-pointing things | Dilip Sequiera | |
| 1996-12-05 | added variable pbp-mode-is so that pbp-mode can be inherited | Thomas Kleymann | |
| 1996-12-05 | added font-lock properties for pbp-lego-mode | Thomas Kleymann | |
| 1996-12-03 | added pbp-mode | Thomas Kleymann | |
| 1996-12-03 | Invisible pbp command handling | Dilip Sequiera | |
| 1996-12-03 | minor extensions of regular expressions | Thomas Kleymann | |
| 1996-12-03 | Minor fix for performance reasons. | Dilip Sequiera | |
| 1996-12-03 | A few small fixes to deal with performance problems. | Dilip Sequiera | |
| 1996-11-29 | removed debug information | Thomas Kleymann | |
| 1996-11-29 | o added logical macros as keywords | Thomas Kleymann | |
| o removed keywords SaveFrozen and SaveUnfrozen o fixed bug in lego-outline-regexp | |||
| 1996-11-22 | pbp.el succeeds ext.el | Thomas Kleymann | |
| 1996-11-22 | A generic package for proof-by-pointing | Thomas Kleymann | |
| 1996-11-22 | *** empty log message *** | Thomas Kleymann | |
| 1996-11-21 | Synchro bug fixed. | Dilip Sequiera | |
| 1996-11-21 | *** empty log message *** | Thomas Kleymann | |
| 1996-11-18 | Fixed Undo problem, now prettifies output, and deals a bit more gracefully | Dilip Sequiera | |
| with errors. | |||
| 1996-11-17 | Cleaned ext.el up a bit in terms of its namespace and the management of | Dilip Sequiera | |
| the comint filter. | |||
| 1996-11-13 | minor changes regarding regular expressions | Thomas Kleymann | |
| 1996-11-13 | Fixed parenthesis matching to deal with comments | Dilip Sequiera | |
| 1996-11-13 | Yves Bertot: | Thomas Kleymann | |
| If you click on an hypothesis name or a goal name, then Emacs generates commands that are sent to lego but not stored in the script buffer. The fix I have is to replace pbp-construct-command | |||
| 1996-11-13 | Yves Bertot's extension for proof by pointing. These should probably | Thomas Kleymann | |
| be integrated in the generic proof package. | |||
| 1996-11-13 | Yves Bertot's proof by pointing | Thomas Kleymann | |
| 1996-11-12 | improved lego-outline-regexp | Thomas Kleymann | |
| 1996-11-10 | fix for incorrect lego-outline-regexp | Thomas Kleymann | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |