proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2013-01-21	- implement proof-script insertion	Hendrik Tews

2013-01-20	- implement retract from prooftree	Hendrik Tews

2013-01-17	- support Grab Existential Variables for Prooftree	Hendrik Tews
	- protocol change, but stay at version 3
2013-01-15	- support bullets and braces in Prooftree	Hendrik Tews
	- prooftree protocol change to version 3
2012-09-12	treat #450 by requiring that proofs are started with Proof	Hendrik Tews

2012-01-19	Typo	David Aspinall

2012-01-04	* fix case where some existential is instantiated with the last proof command	Hendrik Tews
	* protocol change - rename proof-complete into proof-finished and add existential info - add proof-complete message
2012-01-03	merge ProofTreeBranch into main trunk:	Hendrik Tews
	- add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof