aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
1998-05-21Initialize 'before pointer in add-span-aux when last-span is nil.Healfdene Goguen
1998-05-19Removed indentation problem.Healfdene Goguen
1998-05-19Added header and log message.Healfdene Goguen
1998-05-19Added header and log message.Healfdene Goguen
1998-05-19Changed proof-indent-line code so that it doesn't modify buffer ifHealfdene Goguen
1998-05-16*** empty log message ***Thomas Kleymann
1998-05-16implementation of `lego-shell-adjust-line-width' can now be called asThomas Kleymann
1998-05-15Added problem with indentation.Healfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-15Changed variable names [s]ext to span.Healfdene Goguen
1998-05-15Changed variable names [s]ext to span.Healfdene Goguen
1998-05-15Added CoFixpoint and tactics.Healfdene Goguen
1998-05-14Changes to indentation code:Healfdene Goguen
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
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
1998-05-12Added hook `coq-shell-init-hook', for `proof-shell-insert-hook'.Healfdene Goguen
1998-05-08Made separated indentation more elegant:Healfdene Goguen
1998-05-08Made separated indentation more elegant.Healfdene Goguen
1998-05-08Made separated indentation more elegant.Healfdene Goguen
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 12:15:18 +0000