proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2013-05-31	Documentation of ML4PG	joheras

2013-05-30	ML4PG functionality added to Coq menu	joheras

2013-05-30	* empty log message *	joheras

2013-05-30	Adding some more standard utf8 symbols to indentation operator. We	Pierre Courtieu
	really need some "operator" recognition here.
2013-05-29	Fixing a minor bug in indetation (exists is tactic and a quantifier).	Pierre Courtieu

2013-05-23	Run make check before release	David Aspinall

2013-05-22	make warnings non-fatal for normal compilation to fix #458, use	Hendrik Tews
	'make check' to get errors
2013-05-22	rename ProofGeneral.{jpg,gif} into ProofGeneral-image.{jpg,gif}	Hendrik Tews
	to fix #472
2013-05-22	Retire Serifa font usage	David Aspinall

2013-05-22	Set version tag for new release.	David Aspinall

2013-05-22	Add ProofGeneral.jpg to distribution	David Aspinall

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