aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
1998-05-08Merged indentation code for LEGO and Coq into proof.el.Healfdene Goguen
1998-05-08Merged indentation code for LEGO and Coq into proof.el.Healfdene Goguen
1998-05-06Fixed bug with inserting commands and proof-shell-config.Healfdene Goguen
1998-05-06Removed default instantiation of undo limit to 100.Healfdene Goguen
1998-05-06Added comments about info file and default values in coq.el.Healfdene Goguen
1998-05-06Removed proof-dependencies-emacs19 for the moment, since not having itHealfdene Goguen
1998-05-06Fixed problem introduced by working on emacs19 inHealfdene Goguen
1998-05-06Changed lego-undoable-commands-regexp to have "andI" and "andE"Healfdene Goguen
1998-05-06First checked-in version.Healfdene Goguen
1998-05-06Basic description of script management, in texinfo format.Healfdene Goguen
1998-05-06Basic description of script management, compiled for emacs info mode.Healfdene Goguen
1998-05-06Added lego-info-dir so that location of script-management.info can beHealfdene Goguen
1998-05-06Added coq-info-dir so that script-management.info can be hard-coded.Healfdene Goguen
1998-05-06Simpler procedure for compiling emacs lisp.Healfdene Goguen
1998-05-05Coq now restarts if going back to beginning of proof.Healfdene Goguen
1998-05-05Updated to include changes for emacs19.Healfdene Goguen
1998-05-05Simple white-space changes.Healfdene Goguen
1998-05-05Removed because its functionality is subsumed by the xemacs andHealfdene Goguen
1998-05-05Dependencies of proof mode for xemacsHealfdene Goguen
1998-05-05Dependencies of proof mode for emacs19Healfdene Goguen
1998-05-05Added lego-goal-command-p to fix Coq's problem with "Definition".Healfdene Goguen
1998-05-05Made updates to fix problem with Definition, which couldn't beHealfdene Goguen
1998-05-05Added CoInductive.Healfdene Goguen
1998-05-05Basic instructions that come with packageHealfdene Goguen
1998-05-01This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
1998-05-01X-Symbol version 4.45 betaDavid Aspinall
1998-05-01This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
1998-05-01Version 4.5 (beta?) sent by CW, as a package distrib.David Aspinall
1998-04-27removed explicit reference to a binary in ctm's home directoryThomas Kleymann
1998-04-17X-Symbol version 4.45 betaDavid Aspinall
1998-04-17This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
1998-04-17Version 4.5 (beta?) sent by CW, as a package distrib.David Aspinall
1998-04-17This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
1998-03-25added support for etags at generic proof levelThomas Kleymann
1998-03-24*** empty log message ***Thomas Kleymann
1998-02-11prioritisedThomas Kleymann
1998-02-10*** empty log message ***Thomas Kleymann
1998-02-10added Dnf to lego-undoable-commands-regexpThomas Kleymann
1998-01-26X-Symbol version 4.45 betaDavid Aspinall
1998-01-26This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
1998-01-16Commented the code of proof.el and lego.el a bit. Made a minor changeDilip Sequiera
1998-01-15Added coq-shell-cdHealfdene Goguen
1998-01-15Updated method of defining proof-shell-cd to be consistent with otherHealfdene Goguen
1998-01-15One needed change for coq includedHealfdene Goguen
1998-01-12o added support for remote proof processesThomas Kleymann
1998-01-05improved fume supportThomas Kleymann
1998-01-05fixed a bug in the indenting functionsThomas Kleymann
1997-12-18*** empty log message ***Thomas Kleymann
1997-12-18o introduced proof-shell-handle-error-hook and bount it by default toThomas Kleymann
1997-11-26Noted bug in popup-eager-annotationDilip Sequiera
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-22 08:43:21 +0000