proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Failed attempt to prevent Coq from starting up with display of current ↵	David Aspinall	1999-09-13
\| \| \| \|	directory.
*	Cleaned up example files so all demonstrate same theorem "conj_comms".	David Aspinall	1999-09-13
\| \| \| \| \|	Would be nice to add more theorems to compare scripts in different systems.
*	Set proof-{qed,save}-commands.	David Aspinall	1999-09-13
\|
*	Updated from Coq 6.3 distrib.	David Aspinall	1999-08-23
\|
*	Updates suggested by Markus and Patrick for Coq 6.3.	David Aspinall	1999-08-23
\|
*	fixed some regexp via proof-anchor-regexp;	Makarius Wenzel	1999-07-02
\|
*	Missing parentheses added. Docstring fix.	David Aspinall	1999-06-30
\|
*	last commit for 2.1	Patrick Loiseleur	1999-06-30
\|
*	keywords of coq 6.3	Patrick Loiseleur	1999-06-30
\|
*	Hints Resolve	Patrick Loiseleur	1999-06-21
\|
*	better syntax	Patrick Loiseleur	1999-06-16
\|
*	Various updates. coq-end-Section now works properly.	Patrick Loiseleur	1999-06-14
\|
*	More colors, more regexps, more keywords	Patrick Loiseleur	1999-06-09
\|
*	various fixes	Patrick Loiseleur	1999-06-08
\|
*	renamed proof-commands-regexp to proof-indent-commands-regexp, which	Makarius Wenzel	1999-05-27
\| \| \| \|	is less confusing);
*	closed string in comment;	Makarius Wenzel	1999-05-26
\|
*	I've added the custom option 'prog-name-guess' in the generic part and	Patrick Loiseleur	1999-05-17
\| \| \| \| \| \| \| \| \|	the function coq-guess-command-line in the coq part. Every prover should have the functon *-guess-command-line that uses, for example, the output of "make -n" to guess the correct command line options of the prover. Patrick
*	several additions, as usual	Patrick Loiseleur	1999-05-17
\|
*	OrElse -> Orelse	Patrick Loiseleur	1999-05-03
\|
*	proof-list-global is disabled (must be rewritten)	Patrick Loiseleur	1999-05-03
\|
*	Added the correct proof-shell-restart-cmd	Patrick Loiseleur	1999-04-20
\|
*	A few coloring tricks	Patrick Loiseleur	1999-04-20
\|
*	Merged changes sent by Patrick Loiseleur.	David Aspinall	1999-04-07
\|
*	Comments from Healf explaining need for coq-goal-command-p	David Aspinall	1999-02-22
\|
*	fixed syntax entry for "_"	Thomas Kleymann	1999-02-03
\|
*	Use proof-string-match in (hopefully) appropriate places	David Aspinall	1999-02-01
\|
*	radical new version of Credits and References section	Thomas Kleymann	1998-12-15
\|
*	made many minor changes to the documentation	Thomas Kleymann	1998-12-15
\|
*	Added note about removing proof-goal-command-p	David Aspinall	1998-11-12
\|
*	Removed references of proof-shell-noise-regexp	Thomas Kleymann	1998-11-10
\|
*	fixed bug with font-lock face names	Thomas Kleymann	1998-11-03
\|
*	fixed minor bugs	Thomas Kleymann	1998-11-02
\|
*	o added support for byte-compilation	Thomas Kleymann	1998-11-01
\| \| \| \| \| \| \|	o removed hhg tags in todo o fixed font-lock for FSF Emacs 20.2 o ensured that goals buffer is updated for longer queues o fixed a bug in proof-universal-keys-only-mode
*	More hacks to variable names for customize (sorry)	David Aspinall	1998-10-29
\|
*	Begun work on clean byte compilation / clarifying interfaces.	David Aspinall	1998-10-27
\|
*	Renamed proof-invisible-command proof-shell-invisible-command.	David Aspinall	1998-10-27
\| \| \| \| \| \| \|	Removed superfluous optional 'relaxed' argument from: proof-shell-invisibile-command, proof-grab-lock, proof-start-queue.
*	Change to proof-shell-ready-prover	David Aspinall	1998-10-26
\|
*	Added proof-mode-for-script setting.	David Aspinall	1998-10-23
\|
*	Replaced remaining face defs with defface calls.	David Aspinall	1998-10-23
\| \| \| \| \|	Removed font-lock-<newface> with proof-<newface> so we know where things come from and won't break future font locks.
*	support for nested goals is now restricted to Coq	Thomas Kleymann	1998-10-18
\|
*	Removed coq-settings defgroup, changed to coq.	David Aspinall	1998-10-07
\| \| \| \| \| \|	Defcustom'd coq-prog-name. Removed proof-assistant setting (now automatic) Added FIXME question about proof-shell-init-cmd.
*	changed maintainer information to lego@dcs and isabelle@dcs .	Thomas Kleymann	1998-10-02
\|
*	Updated maintainer tags to remove lego email address.	David Aspinall	1998-10-01
\|
*	Replaced string COMMENT by constant proof-no-command.	David Aspinall	1998-10-01
\|
*	coqtags is now Perl5 compatible - courtesy of hhg	Thomas Kleymann	1998-10-01
\|
*	Example file suggested by Healf.	David Aspinall	1998-09-23
\|
*	Removed history	David Aspinall	1998-09-23
\|
*	Removed history, added branding.	David Aspinall	1998-09-23
\|
*	Fixed docstrings for derived modes	David Aspinall	1998-09-22
\|
*	Added Id to headers.	David Aspinall	1998-09-09
\|