| Age | Commit message (Collapse) | Author |
|---|
|
* pbp-goal-command and pbp-hyp-command use proof-terminal-string
* updates to keywords
* fix for goal regexp
|
|
|
|
|
|
|
|
fontified first.
Added "Print" to list of commands.
|
|
Hence, << Cd "../x". >> works in Coq, and
<< echo "hello; world"; >> should work in LEGO
But maybe we don't want "Cd"'s at all...
|
|
continuous pbp-buffer update bug.
|
|
Changed ";" to "." in coq-save-with-hole-regexp
New modifications to syntax table to reflect actual use of symbols in Coq
|
|
|
|
doesn't work when you are inside a comment and press the
proof-terminal-char
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
