proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	added some comments in coq/todo	Pierre Courtieu	2000-09-29
\|
*	Make default path to perl be /usr/bin/perl	David Aspinall	2000-09-29
\|
*	a little change in coq/x-symbol, nothing	Pierre Courtieu	2000-09-29
\|
*	A little work around for the bug of Coq concerning the restart that	Pierre Courtieu	2000-09-29
\| \| \| \| \| \| \|	uses Reset Initial which doesn't reset the Implicit Arguments flag to Off (this is the bug), I added the good command to the coq reset command, this has to be backtracked when V7 will be done (the bug is already corrected in V7).
*	Added Uncaught exception errors in coq-error-regexp.	Pierre Courtieu	2000-09-29
\|
*	Updated from doc	David Aspinall	2000-09-27
\|
*	nothing important, I forgot to undo something before my last commit in	Pierre Courtieu	2000-08-26
\| \| \| \|	coq/x-symbol-coq.el
*	Some changes for undoing with coq, handle user-defined tactics, in	Pierre Courtieu	2000-08-26
\| \| \| \|	coq/coq-syntax.el and coq/coq.el.
*	enhancement of outline regexps for coq, now when hiding bodies, we see	Pierre Courtieu	2000-08-14
\| \| \| \| \|	completely definitions and theorems, but proof script are hidden (but can be blindly sent to the prover). Seems to work correctly.
*	enhancement of x-symbol for coq, philosophy is not encoded, and phi1 is,	Pierre Courtieu	2000-08-14
\| \| \| \|	one problem remains: a word ending with phi will be encoded.
*	Removed some (hopefully redundant) requires.	David Aspinall	2000-07-16
\|
*	somme little changes to make undo work better	Pierre Courtieu	2000-06-22
\|
*	basic setup for new indentation code;	Makarius Wenzel	2000-06-08
\|
*	proper indentation;	Makarius Wenzel	2000-06-08
\|
*	Added 3 entries in the Coq menu: Print Check and Hints	Pierre Courtieu	2000-06-02
\|
*	Removed time setting, added proof-assistant-settings-cmd to init string, but ↵	David Aspinall	2000-06-01
\| \| \| \|	commented out
*	Added a couple of settings for Coq	David Aspinall	2000-06-01
\|
*	Removed use of proof-terminal-string, added explicit terminators everywhere.	David Aspinall	2000-05-29
\|
*	Changed keybindings for coq specific functions	David Aspinall	2000-05-29
\|
*	proof-defass-default -> defpgdefault	David Aspinall	2000-05-26
\|
*	Spurious newline causing patch to fall over.	David Aspinall	2000-05-25
\|
*	Revert to previous path for perl, better default for non-linux. Linux uses ↵	David Aspinall	2000-05-25
\| \| \| \|	RPM, where its fixed.
*	Change default path to perl	David Aspinall	2000-05-25
\|
*	debugging coq menu for old Xemacs compatibility, David said he will do this	Pierre Courtieu	2000-05-16
\| \| \| \|	for other provers (already done ?).
*	Changes and compatibility fixes for specific menu/keybindings.	David Aspinall	2000-05-11
\|
*	Added proof-assistant-keymap and commands for defining insert keys.	David Aspinall	2000-05-02
\|
*	Added specific menu for Coq.	David Aspinall	2000-05-01
\|
*	pbp-mode -> goals-mode	David Aspinall	2000-04-07
\|
*	More decoration	David Aspinall	2000-04-07
\|
*	Fixed up proof-shell-proof-completed mess nicely.	David Aspinall	2000-04-07
\|
*	3.1 not 3.2 change	David Aspinall	2000-03-24
\|
*	Removed spurious requires	David Aspinall	2000-03-24
\|
*	Updated to add me.	David Aspinall	2000-03-23
\|
*	Updated todo's.	David Aspinall	2000-03-22
\|
*	Switch back to %s, rename proof-shell-string-escapes -> ↵	David Aspinall	2000-03-22
\| \| \| \|	proof-shell-filename-escapes, and always apply for filename substn.
*	Altered syntax a little bit so reset works for Section.	David Aspinall	2000-03-19
\|
*	Updated	David Aspinall	2000-03-19
\|
*	Added settings for silent control. Also some minor support for Section.	David Aspinall	2000-03-19
\|
*	Note about useless output from Coq	David Aspinall	2000-03-14
\|
*	Added proof-shell-{start,stop}-silent-cmd.	David Aspinall	2000-03-14
\|
*	BUGS for Coq.	David Aspinall	2000-03-13
\|
*	New/updated information files	David Aspinall	2000-03-13
\|
*	Updated headers.	David Aspinall	2000-03-09
\|
*	Added README files for each prover, summarizing status.	David Aspinall	2000-03-09
\|
*	Split low-level todo into several files.	David Aspinall	2000-03-08
\|
*	Fixes for short output duplication problem: set ↵	David Aspinall	2000-01-06
\| \| \| \|	proof-shell-eager-annotation-start-length.
*	Use auto multiple files until something better comes along	David Aspinall	1999-11-16
\|
*	Remove xi, appears in exists.	David Aspinall	1999-11-15
\|
*	Added some greek letters. A mess if they occur in words.	David Aspinall	1999-11-15
\|
*	Removed font-lock settings. Set proof-font-lock-zap-commas=t	David Aspinall	1999-11-15
\|