| Age | Commit message (Collapse) | Author |
|---|
|
|
|
o fixed a bug in lego-find-and-forget due to new treatment of comments
|
|
proof-assert-until-point (it was broken and looks healthier now)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
branch.
|
|
|
|
branch.
|
|
|
|
hence pbp-construct-command does not need to bother to cater for "Next"
command
|
|
|
|
|
|
the pbp package
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
o removed keywords SaveFrozen and SaveUnfrozen
o fixed bug in lego-outline-regexp
|
|
|
|
|
|
|
|
|
|
|
|
with errors.
|
|
the comint filter.
|
|
|
|
|
|
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
|
|
be integrated in the generic proof package.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
moved some bindings from lego-mode-map to proof-mode-map
|
|
|
|
|
