proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Clean whitespace	David Aspinall	2009-09-05
\|
*	Remove some old X-Symbol references.	David Aspinall	2009-09-01
\|
*	Merge changes from Version4Branch.	David Aspinall	2008-07-24
\|
*	Fixed indentation and goal display.	Pierre Courtieu	2008-01-28
\|
*	Patch and cleanup for Coq indent code, see ↵	David Aspinall	2008-01-25
\| \| \| \|	http://proofgeneral.inf.ed.ac.uk/trac/ticket/173
*	Missing paren	David Aspinall	2008-01-24
\|
*	Fixes and cleanups for coq-indent-line, see Trac #172	David Aspinall	2008-01-24
\|
*	Remove proof-indent-pad-eol atrocity	David Aspinall	2007-02-28
\|
*	typo in coq-indent.	Pierre Courtieu	2006-09-15
\|
*	fixed a typo in last correction.	Pierre Courtieu	2006-09-15
\|
*	fixed a bug from Stefan Monnier.	Pierre Courtieu	2006-09-14
\|
*	cleaning from Stefan Monnier.	Pierre Courtieu	2006-09-13
\|
*	cleaning from Stefan Monnier.	Pierre Courtieu	2006-09-13
\|
*	Fixed nested comment support for scripting, in xemacs (worked already	Pierre Courtieu	2006-09-08
\| \| \| \|	on GNU Emacs). Instanciated proof-parse-function for that...
*	Trying to mae indentation aware of nested comments (to be simplified	Pierre Courtieu	2006-09-04
\| \| \| \| \|	when xemacs will deal with nested comments). Seems to work, a bit slow.
*	Fixed a small bug in indentation of coq.	Pierre Courtieu	2006-08-25
\| \| \| \|	Fixed behavior for making abbrev table (don't if it already exists).
*	fixing a bug introduced lately (coq-save-command-p needs two args	Pierre Courtieu	2006-08-24
\| \| \| \|	beacause proof-save-command-p needs is so defined).
*	Fixed indentation and font-lock for coq. Better, faster.	Pierre Courtieu	2006-08-23
\|
*	Coq indentation small fixes.	Pierre Courtieu	2006-08-23
\|
*	fsf emacs compatibilty for symbol-at-point.	Pierre Courtieu	2006-08-23
\|
*	removed debug messages from indentation code.	Pierre Courtieu	2006-07-04
\|
*	fix the bug for coq indetation of two consecutive comments. Code is	Pierre Courtieu	2006-07-04
\| \| \| \| \|	ugly, should take the code given by Stefan Monnier and adapt it (it does not indent everything as is).
*	fix a bug in coq indentation (loop). seems to be fixed. I still have a	Pierre Courtieu	2006-07-04
\| \| \| \|	problem indenting comments (two consecutive comments: second shifted).
*	moving coq-goal-command-p to indetation code, as from v8.1, goals are	Pierre Courtieu	2006-07-04
\| \| \| \| \| \|	detected by the goal attribute of spans. syntactical goal recognizing is still used in indetation code, and for v8.0 compatibility. I shall remove v8.0 compatibility in some months.
*	added match...with automatic building from atype name.	Pierre Courtieu	2005-11-07
\| \| \| \|	Had to correct a bug in proof-shell.
*	Finished making holes.el a real minor-mode. There is a new file	Pierre Courtieu	2005-02-15
\| \| \| \| \| \| \| \| \|	holes-load.el which defines the autoloads (enough of them?). All functions have the prefix "holes-", and offending keyboard shortcuts have been either removed or bound to the minor mode. I made holes-mode minor mode automatically turned on in all proof buffers in coq mode (including shell, script and response buffers as it may be useful to copy paste parts of this buffers into holes).
*	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).
*	added the forall x-symbol to the indent keywords lists.	Pierre Courtieu	2004-03-30
\|
*	bug fix in holes (call to proof-indent-line instead of funcall	Pierre Courtieu	2004-03-15
\| \| \| \|	indent-line-function).
*	little bug fix in coq-indent.el	Pierre Courtieu	2004-03-15
\|
*	bug fixes on indenting and command-end-regexp.	Pierre Courtieu	2004-03-11
\|
*	compile warning corrections	Pierre Courtieu	2004-03-10
\|
*	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.