proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Updated.	David Aspinall	2010-08-13
\|
*	Remove deliberately buggy code at the end (Coq seems to be fixed)	David Aspinall	2010-08-11
\|
*	Small fixes from Stefan Monnier.	Pierre Courtieu	2007-04-16
\|
*	Changed the type of proof-goal-command-p. It takes now a span, which	Pierre Courtieu	2006-04-26
\| \| \| \| \| \|	allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
*	debugged the indentation of coq (bug report of Batsiaan Zapf august	Pierre Courtieu	2004-08-30
\| \| \| \| \|	3rd 2004). I found another bug (infinite loop due to an error in coq-back-to-indentation-prevline).
*	Update to Coq 8.0 syntax	David Aspinall	2004-04-22
\|
*	Use official indentation\!	David Aspinall	2004-04-02
\|
*	indentation for coq completely re-coded, because the generic mechanism	Pierre Courtieu	2004-03-08
\| \| \| \|	does not use "proof-goal-command-p" and is not powerful enough.
*	corrected a bug of pg/coq, the following line was not recognized as a	Pierre Courtieu	2003-02-20
\| \| \| \| \| \| \| \| \|	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).
*	code cleaning + deals better with the new module system of Coq. Did	Pierre Courtieu	2003-02-03
\| \| \| \|	not test the fsfemacs. Will do before release.
*	Added a file for testing modules of coq (new version 7.4). Plus some	Pierre Courtieu	2003-01-29
	modification to better backtrack modules.