proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2013-05-14	- update coq example	Hendrik Tews
	- minor changes in user manual
2013-05-10	Set version tag for new release.	David Aspinall

2013-04-19	improve doc	Hendrik Tews

2013-03-27	add 4.3 news to user manual	Hendrik Tews

2013-03-27	Set version tag for new release.	David Aspinall

2013-03-05	fix overwriting the empty compilation queue	Hendrik Tews

2013-02-20	small improvement	Hendrik Tews

2013-02-18	fix parallel Coq compilation: report error for circular dependencies	Hendrik Tews

2013-02-18	move message about killing coq compilation processes	Hendrik Tews

2013-02-18	updated TAGS	Hendrik Tews

2013-01-28	Update timestampes	David Aspinall

2013-01-21	- implement proof-script insertion	Hendrik Tews

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

2013-01-17	Fixed a bug with window height optimization.	Pierre Courtieu
	When using unicode symbols, window-height (which is deprecated anyway) is incorrect, using window-text-height instead seems better.
2013-01-17	document latest changes	Hendrik Tews

2013-01-17	- support Grab Existential Variables for Prooftree	Hendrik Tews
	- protocol change, but stay at version 3
2013-01-15	fix overriding distclean target	Hendrik Tews

2013-01-15	removal of backup files (*~) moved to make distclean	Hendrik Tews

2013-01-15	- support bullets and braces in Prooftree	Hendrik Tews
	- prooftree protocol change to version 3
2013-01-11	Set version tag for new release.	David Aspinall

2013-01-10	fix parallel overlapping calls of proof-shell-filter	Hendrik Tews

2013-01-03	- fix asserting when parallel background compilation is in progress	Hendrik Tews
	- fix aborting background compilation on error
2012-11-15	write CHANGES	Hendrik Tews

2012-11-14	- fix problem in emergency process killing	Hendrik Tews
	- better handling of errors in process creation
2012-11-14	all-cpus option for coq-max-background-compilation-jobs	Hendrik Tews

2012-11-14	fix coq-lock-ancestor for parallel compilation	Hendrik Tews

2012-11-14	update documentation	Hendrik Tews

2012-11-13	update TAGS	Hendrik Tews

2012-11-13	- first version of parallel asynchronous compilation for coq in	Hendrik Tews
	coq-par-compile.el (must be activated via coq-compile-parallel-in-background) - items in the queue region are not necessarily in proof-action-list any more! Require commands and the following items are stored elsewhere until the compilation finishes. Variable proof-second-action-list-active notifies the generic machinery if queue items are stored elsewhere. In this case, Proof General must neither release the proof shell lock nor delete the queue span when proof-action-list is empty. - to kill background processes as early as possible, the new hook proof-shell-signal-interrupt-hook is used
2012-11-13	small typo fixes	Hendrik Tews

2012-11-09	Doc for pg-finish-tracing-display	David Aspinall

2012-11-06	move ancestor locking back into specific part	Hendrik Tews

2012-11-05	move ancestor locking/unlocking to coq-compile-common	Hendrik Tews

2012-11-05	fix seq-seq misspelling	Hendrik Tews

2012-11-05	move buffer saving to coq-compile-common	Hendrik Tews

2012-11-03	make coq-include-options independent of current buffer	Hendrik Tews

2012-11-03	move another 2 functions into coq-compile-common	Hendrik Tews

2012-11-01	move function for coq-compile-response-buffer to coq-compile-common.el	Hendrik Tews

2012-11-01	Update	David Aspinall

2012-10-30	rename entities in coq-seq-compile	Hendrik Tews

2012-10-30	move some more material into coq-compile-common	Hendrik Tews

2012-10-30	update TAGS	Hendrik Tews

2012-10-30	move general part of compilation into coq-compile-common.el	Hendrik Tews

2012-10-30	move coq compilation into coq/coq-seq-compile.el	Hendrik Tews

2012-10-19	Set version tag for new release.	David Aspinall

2012-10-19	Updates for PG 4.3	David Aspinall

2012-10-19	Set version tag for new release.	David Aspinall

2012-10-03	"as" insertion on a region.	Pierre Courtieu

2012-10-03	Fixed auto-insert-as stuff + fix compiling problems.	Pierre Courtieu

2012-10-02	Made 'as' automatic insertion a togglable feature (not finished) (2).	Pierre Courtieu