index
:
proof-general
master
Emacs plugins for proof management systems
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
1998-06-02
Structured review now done.
Healfdene Goguen
1998-06-02
Corrected comment about this being for emacs19.
Healfdene Goguen
1998-06-02
Corrected comment about this being for xemacs.
Healfdene Goguen
1998-06-02
Added comment about C-c ' that it will switch to the scripting buffer.
Healfdene Goguen
1998-06-02
Generalized proof-retract-target, now parameterized by
Healfdene Goguen
1998-06-02
Generalized proof-retract-target, now parameterized by
Healfdene Goguen
1998-06-02
Minor modifications to comments
Healfdene Goguen
1998-05-29
fixed a bug in `proof-goto-end-of-locked-if-pos-not-visible-in-window'
Thomas Kleymann
1998-05-29
o outsourced indentation to proof-indent
Thomas Kleymann
1998-05-26
Necessary changes for emacs19 version
Healfdene Goguen
1998-05-26
Removed commented code in proof-dont-show-annotations
Healfdene Goguen
1998-05-23
improved support for Info
Thomas Kleymann
1998-05-22
Correct path for coq-prog-name and coq-tags.
Healfdene Goguen
1998-05-22
fixed a bug in proof-frob-locked-end
Thomas Kleymann
1998-05-22
included "Invert" in `lego-keywords'
Thomas Kleymann
1998-05-21
Made proof-locked-span and proof-queue-span buffer-local.
Healfdene Goguen
1998-05-21
Removed uninitialized os variable in spans-at-region.
Healfdene Goguen
1998-05-21
Changing buffers now works.
Healfdene Goguen
1998-05-21
Fixed lifting globals.
Healfdene Goguen
1998-05-21
Initialize 'before pointer in add-span-aux when last-span is nil.
Healfdene Goguen
1998-05-19
Removed indentation problem.
Healfdene Goguen
1998-05-19
Added header and log message.
Healfdene Goguen
1998-05-19
Added header and log message.
Healfdene Goguen
1998-05-19
Changed proof-indent-line code so that it doesn't modify buffer if
Healfdene Goguen
1998-05-16
*** empty log message ***
Thomas Kleymann
1998-05-16
implementation of `lego-shell-adjust-line-width' can now be called as
Thomas Kleymann
1998-05-15
Added problem with indentation.
Healfdene Goguen
1998-05-15
Dependencies on versions of emacs have been moved to span-extent.el
Healfdene Goguen
1998-05-15
Dependencies on versions of emacs have been moved to span-extent.el
Healfdene Goguen
1998-05-15
Dependencies on versions of emacs have been moved to span-extent.el
Healfdene Goguen
1998-05-15
Dependencies on versions of emacs have been moved to span-extent.el
Healfdene Goguen
1998-05-15
Changed variable names [s]ext to span.
Healfdene Goguen
1998-05-15
Changed variable names [s]ext to span.
Healfdene Goguen
1998-05-15
Added CoFixpoint and tactics.
Healfdene Goguen
1998-05-14
Changes to indentation code:
Healfdene Goguen
1998-05-14
Updated install script after finding problems with Savi's setup.
Healfdene Goguen
1998-05-13
revised in light of today's meeting with hhg
Thomas Kleymann
1998-05-12
Added documentation for C-c C-s in Coq mode.
Healfdene Goguen
1998-05-12
Added documentation for C-c C-s in Coq mode.
Healfdene Goguen
1998-05-12
Added hook `proof-shell-insert-hook', to replace `proof-shell-config'.
Healfdene Goguen
1998-05-12
Added hook `proof-shell-insert-hook', which is initalized to
Healfdene Goguen
1998-05-12
Added hook `coq-shell-init-hook', for `proof-shell-insert-hook'.
Healfdene Goguen
1998-05-08
Made separated indentation more elegant:
Healfdene Goguen
1998-05-08
Made separated indentation more elegant.
Healfdene Goguen
1998-05-08
Made separated indentation more elegant.
Healfdene Goguen
1998-05-08
Merged indentation code for LEGO and Coq into proof.el.
Healfdene Goguen
1998-05-08
Updated todo list.
Healfdene Goguen
1998-05-08
Merged indentation code for LEGO and Coq into proof.el.
Healfdene Goguen
1998-05-08
Merged indentation code for LEGO and Coq into proof.el.
Healfdene Goguen
1998-05-06
Fixed bug with inserting commands and proof-shell-config.
Healfdene Goguen
[next]