aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
1998-05-08Made separated indentation more elegant:Healfdene Goguen
Made proof-assistant specific code into separate procedure, proof-parse-indent. Separated consideration of {}'s so it only happens for LEGO.
1998-05-08Made separated indentation more elegant.Healfdene Goguen
Separated consideration of {}'s so it only happens for LEGO.
1998-05-08Made separated indentation more elegant.Healfdene Goguen
Fixed bug with Inductive. Added CoInductive.
1998-05-08Merged indentation code for LEGO and Coq into proof.el.Healfdene Goguen
1998-05-08Updated todo list.Healfdene Goguen
1998-05-08Merged indentation code for LEGO and Coq into proof.el.Healfdene Goguen
Fixed problem with active terminator mode: [proof-terminal-char] isn't the same as (vector proof-terminal-char).
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
introduces error messages. Put cd before init in proof-shell-config-done (this won't work for Coq).
1998-05-06Fixed problem introduced by working on emacs19 inHealfdene Goguen
proof-zap-commas-region.
1998-05-06Changed lego-undoable-commands-regexp to have "andI" and "andE"Healfdene Goguen
instead of "AndI" and "AndE".
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
hard-coded.
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
Added coq-info-dir so that script-management.info can be hard-coded.
1998-05-05Coq now restarts if going back to beginning of proof.Healfdene Goguen
1998-05-05Updated to include changes for emacs19.Healfdene Goguen
Also includes some changes for "Definition" problem in Coq, where Definition couldn't be used for proof scripts. Finally, modified proof-dependencies-xemacs code to fix problem that undoing to (point-min) meant you couldn't type at first character.
1998-05-05Simple white-space changes.Healfdene Goguen
1998-05-05Removed because its functionality is subsumed by the xemacs andHealfdene Goguen
emacs19 files.
1998-05-05Dependencies of proof mode for xemacsHealfdene Goguen
There may be one or two areas that can be unified with emacs19 dependencies.
1998-05-05Dependencies of proof mode for emacs19Healfdene Goguen
Still in progress!
1998-05-05Added lego-goal-command-p to fix Coq's problem with "Definition".Healfdene Goguen
Removed lego-killref from menu.
1998-05-05Made updates to fix problem with Definition, which couldn't beHealfdene Goguen
used with proof scripts. Removed some useless declarations. Removed Abort from menu. Now Reset's if user undoes to beginning of proof. Added command to increase undo limit for Coq, and set default to 100.
1998-05-05Added CoInductive.Healfdene Goguen
Made updates to reflect problem with "Definition", which couldn't be used with proof scripts.
1998-05-05Basic instructions that come with packageHealfdene Goguen
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
branch.
1998-05-01Version 4.5 (beta?) sent by CW, as a package distrib.David Aspinall
1998-05-01This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
branch.
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
branch.
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
branch.
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
branch.
1998-01-16Commented the code of proof.el and lego.el a bit. Made a minor changeDilip Sequiera
to the way errors are handled, so that any delayed output is inserted in the buffer before the error message is printed.
1998-01-15Added coq-shell-cdHealfdene Goguen
Some new fontlocks
1998-01-15Updated method of defining proof-shell-cd to be consistent with otherHealfdene Goguen
proof-assistant-dependent variables. Added ctrl-button1 to copy selected region to end of locked region
1998-01-15One needed change for coq includedHealfdene Goguen
1998-01-12o added support for remote proof processesThomas Kleymann
o bound C-c C-z to 'proof-frob-locked-end
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-16 08:17:32 +0000