proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Change of proof span type back to goalsave	David Aspinall	2001-08-28
\|
*	Modification of proof-script-command-end-regexp to allow commands	Pierre Courtieu	2001-04-10
\| \| \| \|	ended by ".eof"
*	Added the config var proof-script-command-end-regexp fot coq V7.	Pierre Courtieu	2001-03-20
\|
*	minor change in coq.el to allow to force version of coq, with variable	Pierre Courtieu	2001-02-26
\| \| \| \|	coq-version-is-V7
*	Experimental support for multiple file handling.	David Aspinall	2000-12-20
\| \| \| \|	'goalsave -> 'proof
*	fixed spelling;	Makarius Wenzel	2000-11-27
\|
*	Continuing Coq V7 compatibility work, Begin Silent -> Set Silent, etc...	Pierre Courtieu	2000-11-24
\|
*	Add a little change to coq-find-and-forget to work better	Pierre Courtieu	2000-11-24
\|
*	I am starting to make PG coqV7 compatible, I think the best is to	Pierre Courtieu	2000-11-23
\| \| \| \| \|	allow both V6 and V7 for a while. Theoretically, incompatibilities will not be numerous.
*	Note about alternative path to perl	David Aspinall	2000-10-02
\|
*	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
\|