proof-general - Emacs interface for proof assistants

	Commit message (Expand)	Author	Age
*	Fix compile	David Aspinall	2011-04-26
*	Fix so that make test.coq runs successfully.	David Aspinall	2011-04-26
*	Clean up some defcustom docstrings (remove *'s)	David Aspinall	2011-04-26
*	* fix coq-show-first-goal changing the current buffer	Hendrik Tews	2011-04-15
*	* fix overwriting setq coq-prog-name before loading Proof General	Hendrik Tews	2011-04-15
*	* disable file safe when switching to new buffers for coq	Hendrik Tews	2011-04-06
*	- change to proof-restart-buffers for unlocking ancestors	Hendrik Tews	2011-03-14
*	- fixed XXX'es in coq.el	Hendrik Tews	2011-02-28
*	- adjust coq-ask-insert-coq-prog-name and doc in coq-local-vars-doc	Hendrik Tews	2011-02-28
*	- deleted old coq multiple file stuff	Hendrik Tews	2011-02-18
*	put coq compilation feature into coq settings menu	Hendrik Tews	2011-02-14
*	- properly display compilation error messages and enable M-x	Hendrik Tews	2011-02-02
*	Old debug setting	David Aspinall	2011-01-31
*	- use low-level compilation interface for external coq	Hendrik Tews	2011-01-28
*	- mark new coq specific variables as safe	Hendrik Tews	2011-01-28
*	Clean coq goals buffer when backing to a non-proof state, otherwise	Pierre Courtieu	2011-01-28
*	Add autotest-start with debug for now	David Aspinall	2011-01-26
*	- more info on the elements of proof-action-list; the COMMANDS	Hendrik Tews	2011-01-26
*	- fix 1 second problem	Hendrik Tews	2011-01-26
*	- fix problem description	Hendrik Tews	2011-01-26
*	- unlock files when retracting a Require command (implemented via	Hendrik Tews	2011-01-25
*	Remove proof-shell-wait that causes deadlock with new multiple-file code.	David Aspinall	2011-01-25
*	- use time-less-p	Hendrik Tews	2011-01-21
*	- switch off automatic compilation for coq to not surprise users	Hendrik Tews	2011-01-19
*	- fixed stale load path problem with killing the proof shell in	Hendrik Tews	2011-01-18
*	- implemented coq-lock-ancestors as described in the docs already	Hendrik Tews	2011-01-18
*	Add multiple file test case	David Aspinall	2011-01-18
*	Alternative fix to #382.	David Aspinall	2011-01-18
*	set proof-auto-action-when-deactivating-scripting to 'retract,	David Aspinall	2011-01-18
*	Localise compilation fix for dynamic scope of `queueitems\'.	David Aspinall	2011-01-18
*	- fixed compilation errors	Hendrik Tews	2011-01-18
*	- fix broken external compilation	Hendrik Tews	2011-01-18
*	Fix trac 382 by not setting save-abbrevs.	Pierre Courtieu	2011-01-18
*	fix problems in test cases	Hendrik Tews	2011-01-17
*	- more coq test cases (some with surprising and embarrassing bugs)	Hendrik Tews	2011-01-14
*	Update dates and versions	David Aspinall	2011-01-14
*	- move proof-no-fully-processed-buffer to generic/proof-config	Hendrik Tews	2011-01-14
*	- simple backward compatible change to invoke a function to	Hendrik Tews	2011-01-14
*	- Remove nonfunctional Add LoadPath code.	Hendrik Tews	2011-01-14
*	Add preliminary support for multiple files for coq.	Hendrik Tews	2011-01-12
*	Fix compile problem with smie code on Emacs <=23.3	David Aspinall	2010-11-25
*	Summary: New indentation code using SMIE	Stefan Monnier	2010-11-15
*	Fixed a bug with utf8 error highlighting in coq 8.3 (bugs with 8.2	Pierre Courtieu	2010-10-22
*	Add some more tokens for making pretty pictures	David Aspinall	2010-10-10
*	coq-find-and-forget: Allow undoing prover processed regions	David Aspinall	2010-10-10
*	coq-generic-expression: fix this to match symbols, not merely words.	David Aspinall	2010-10-10
*	Fixes in strings/comments from Erik Martin-Dorel	David Aspinall	2010-10-04
*	coq-insert-solve-tactic: added (credit:Erik Martin-Dorel, patch from trac #35...	David Aspinall	2010-10-04
*	Rename span-add-self-removing-span	David Aspinall	2010-10-01
*	coq-highlight-error: use span-add-self-removing-span (highlight and removal i...	David Aspinall	2010-10-01