proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2010-08-13	Updated.	David Aspinall

2010-08-11	Remove deliberately buggy code at the end (Coq seems to be fixed)	David Aspinall

2007-04-16	Small fixes from Stefan Monnier.	Pierre Courtieu

2006-04-26	Changed the type of proof-goal-command-p. It takes now a span, which	Pierre Courtieu
	allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
2004-08-30	debugged the indentation of coq (bug report of Batsiaan Zapf august	Pierre Courtieu
	3rd 2004). I found another bug (infinite loop due to an error in coq-back-to-indentation-prevline).
2004-04-22	Update to Coq 8.0 syntax	David Aspinall

2004-04-02	Use official indentation\!	David Aspinall

2004-03-08	indentation for coq completely re-coded, because the generic mechanism	Pierre Courtieu
	does not use "proof-goal-command-p" and is not powerful enough.
2003-02-20	corrected a bug of pg/coq, the following line was not recognized as a	Pierre Courtieu
	module start: Module M:T with Definition A:=u. I had to count the number of 'with' and ':=' to know if the last ':=' was a Module given explicitely (--> no module start) or only part of a 'with ...:=' (--> module start).
2003-02-03	code cleaning + deals better with the new module system of Coq. Did	Pierre Courtieu
	not test the fsfemacs. Will do before release.
2003-01-29	Added a file for testing modules of coq (new version 7.4). Plus some	Pierre Courtieu
	modification to better backtrack modules.