| Age | Commit message (Collapse) | Author |
|
o Allowed proof-shell-process-file function to return nil
o Fixed bug (missing declaration of 'file') in
proof-shell-process-urgent-message
|
|
|
|
|
|
|
|
|
|
|
|
|
|
o fixed bug in ...-check-...
|
|
o Fixed bug in proof-toolbar-next
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
COQ: C-c u inside a Section should reset the whole section, then
redo defns
LEGO: consider Discharge; perhaps unrol to the beginning of the
module?
The suggested mechanism subsumes the current setup for normal commands
and goalsave properties.
|
|
|
|
|
|
|
|
|
|
|
|
|