proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2013-07-05	Updating pg documentation about new feature coq project file.	Pierre Courtieu

2013-07-05	Fixing #466. Indent. bug when illformed commment at file beginning.	Pierre Courtieu
	Nasty bug due to smie fallback to backward-sexp when finding an unknown token, namely the token "", which happens when reaching the bof. Had to add a specific token for b o f.
2013-07-05	more appropriate URL;	Makarius Wenzel

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

2013-07-05	Document Make check	David Aspinall

2013-07-04	Fixing a compilation warning for a ml4pg function in coq.el.	Pierre Courtieu

2013-07-04	Fixing undeclared variables for compilation.	Pierre Courtieu

2013-07-02	Added faq for coq pg.	Pierre Courtieu

2013-07-02	Fixing coq project file mechanism.	Pierre Courtieu

2013-06-21	Added an entry to CHANGEs about coq project fields.	Pierre Courtieu

2013-06-19	Adding support for coq project file for setting coqdoc args.	Pierre Courtieu
	second attempt, seems better (cleaner code).
2013-06-19	Adding support for coq project file for setting coqdoc args.	Pierre Courtieu
	First attempt, seems ok.
2013-05-31	Authors of ML4PG	joheras

2013-05-31	Removing files from ML4PG folder	joheras

2013-05-31	Removing ML4PG files from coq folder.	joheras

2013-05-31	Removing ML4PG files from coq folder.	joheras

2013-05-31	Inclusion of ML4PG in coq.el file.	joheras

2013-05-31	Moving ML4PG from coq directory to contrib directory.	joheras

2013-05-31	Remove link in tar file.	David Aspinall

2013-05-31	* empty log message *	joheras

2013-05-31	Removing hidden files of ML4PG.	joheras

2013-05-31	Removing hidden files from ML4PG.	joheras

2013-05-31	ML4PG modification	joheras

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