aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
1998-05-15Changed variable names [s]ext to span.Healfdene Goguen
1998-05-15Changed variable names [s]ext to span.Healfdene Goguen
Fixed coq-find-and-forget pattern for declarations and definitions following Pascal Brisset's suggestion.
1998-05-15Added CoFixpoint and tactics.Healfdene Goguen
Changed indentation.
1998-05-14Changes to indentation code:Healfdene Goguen
Changed "case" to "Case". Added "CoInductive".
1998-05-14Updated install script after finding problems with Savi's setup.Healfdene Goguen
1998-05-13revised in light of today's meeting with hhgThomas Kleymann
1998-05-12Added documentation for C-c C-s in Coq mode.Healfdene Goguen
Fixed problem with tabbing changing buffers.
1998-05-12Added documentation for C-c C-s in Coq mode.Healfdene Goguen
1998-05-12Added hook `proof-shell-insert-hook', to replace `proof-shell-config'.Healfdene Goguen
1998-05-12Added hook `proof-shell-insert-hook', which is initalized toHealfdene Goguen
lego-shell-adjust-line-width. This replaces `lego-shell-config'.
1998-05-12Added hook `coq-shell-init-hook', for `proof-shell-insert-hook'.Healfdene Goguen
This initializes undo limit and changes directory to that associated with buffer. This is because Coq has a command line option to run with emacs mode.
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-01This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
branch.
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 04:18:59 +0000