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-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
1998-05-06
Removed default instantiation of undo limit to 100.
Healfdene Goguen
1998-05-06
Added comments about info file and default values in coq.el.
Healfdene Goguen
1998-05-06
Removed proof-dependencies-emacs19 for the moment, since not having it
Healfdene Goguen
1998-05-06
Fixed problem introduced by working on emacs19 in
Healfdene Goguen
1998-05-06
Changed lego-undoable-commands-regexp to have "andI" and "andE"
Healfdene Goguen
1998-05-06
First checked-in version.
Healfdene Goguen
1998-05-06
Basic description of script management, in texinfo format.
Healfdene Goguen
1998-05-06
Basic description of script management, compiled for emacs info mode.
Healfdene Goguen
1998-05-06
Added lego-info-dir so that location of script-management.info can be
Healfdene Goguen
1998-05-06
Added coq-info-dir so that script-management.info can be hard-coded.
Healfdene Goguen
1998-05-06
Simpler procedure for compiling emacs lisp.
Healfdene Goguen
1998-05-05
Coq now restarts if going back to beginning of proof.
Healfdene Goguen
1998-05-05
Updated to include changes for emacs19.
Healfdene Goguen
1998-05-05
Simple white-space changes.
Healfdene Goguen
1998-05-05
Removed because its functionality is subsumed by the xemacs and
Healfdene Goguen
1998-05-05
Dependencies of proof mode for xemacs
Healfdene Goguen
1998-05-05
Dependencies of proof mode for emacs19
Healfdene Goguen
1998-05-05
Added lego-goal-command-p to fix Coq's problem with "Definition".
Healfdene Goguen
1998-05-05
Made updates to fix problem with Definition, which couldn't be
Healfdene Goguen
1998-05-05
Added CoInductive.
Healfdene Goguen
1998-05-05
Basic instructions that come with package
Healfdene Goguen
1998-05-01
This commit was generated by cvs2git to track changes on a CVS vendor
David Aspinall
1998-05-01
X-Symbol version 4.45 beta
David Aspinall
1998-05-01
This commit was generated by cvs2git to track changes on a CVS vendor
David Aspinall
1998-05-01
Version 4.5 (beta?) sent by CW, as a package distrib.
David Aspinall
1998-04-27
removed explicit reference to a binary in ctm's home directory
Thomas Kleymann
1998-04-17
X-Symbol version 4.45 beta
David Aspinall
1998-04-17
This commit was generated by cvs2git to track changes on a CVS vendor
David Aspinall
1998-04-17
Version 4.5 (beta?) sent by CW, as a package distrib.
David Aspinall
1998-04-17
This commit was generated by cvs2git to track changes on a CVS vendor
David Aspinall
1998-03-25
added support for etags at generic proof level
Thomas Kleymann
1998-03-24
*** empty log message ***
Thomas Kleymann
1998-02-11
prioritised
Thomas Kleymann
1998-02-10
*** empty log message ***
Thomas Kleymann
1998-02-10
added Dnf to lego-undoable-commands-regexp
Thomas Kleymann
1998-01-26
X-Symbol version 4.45 beta
David Aspinall
1998-01-26
This commit was generated by cvs2git to track changes on a CVS vendor
David Aspinall
1998-01-16
Commented the code of proof.el and lego.el a bit. Made a minor change
Dilip Sequiera
1998-01-15
Added coq-shell-cd
Healfdene Goguen
1998-01-15
Updated method of defining proof-shell-cd to be consistent with other
Healfdene Goguen
1998-01-15
One needed change for coq included
Healfdene Goguen
1998-01-12
o added support for remote proof processes
Thomas Kleymann
1998-01-05
improved fume support
Thomas Kleymann
1998-01-05
fixed a bug in the indenting functions
Thomas Kleymann
1997-12-18
*** empty log message ***
Thomas Kleymann
1997-12-18
o introduced proof-shell-handle-error-hook and bount it by default to
Thomas Kleymann
[next]