proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
1998-06-02	Structured review now done.	Healfdene Goguen
	Added item that we need to write proof-retract-file.
1998-05-29	o outsourced indentation to proof-indent	Thomas Kleymann
	o support indentation of commands o replaced test of Emacs version with availability test of specific features o C-c C-c, C-c C-v and M-tab is now available in all buffers
1998-05-26	Necessary changes for emacs19 version	Healfdene Goguen

1998-05-21	Changing buffers now works.	Healfdene Goguen

1998-05-21	Fixed lifting globals.	Healfdene Goguen
	Added problem of buffers and need for incremental adding of tactics in Coq.
1998-05-19	Removed indentation problem.	Healfdene Goguen
	Added comments about current state of emacs19 port.
1998-05-16	* empty log message *	Thomas Kleymann

1998-05-15	Added problem with indentation.	Healfdene Goguen

1998-05-13	revised in light of today's meeting with hhg	Thomas Kleymann

1998-05-12	Added documentation for C-c C-s in Coq mode.	Healfdene Goguen
	Fixed problem with tabbing changing buffers.
1998-05-08	Updated todo list.	Healfdene Goguen

1998-05-05	Coq now restarts if going back to beginning of proof.	Healfdene Goguen

1998-02-11	prioritised	Thomas Kleymann

1998-02-10	* empty log message *	Thomas Kleymann

1998-01-15	One needed change for coq included	Healfdene Goguen

1997-12-18	* empty log message *	Thomas Kleymann

1997-11-26	Noted bug in popup-eager-annotation	Dilip Sequiera

1997-11-26	A few new suggestions	Healfdene Goguen

1997-11-20	Fixed outstanding things to be updated in Coq.	Healfdene Goguen

1997-11-18	Added indentation for lego-mode.	Dilip Sequiera

1997-11-17	Added some magic commands: proof-frob-locked-end, proof-try-command,	Dilip Sequiera
	proof-interrupt-process. Added moving nested lemmas above goal for coq. Changed the key mapping for assert-until-point to C-c RET.