proof-general - Emacs interface for proof assistants

	Commit message (Expand)	Author	Age
*	Fixed outstanding things to be updated in Coq.	Healfdene Goguen	1997-11-20
*	Added lego-global-p as always false, but for consistency with Coq mode.	Healfdene Goguen	1997-11-20
*	Added coq-global-p for global declarations and definitions. These now	Healfdene Goguen	1997-11-20
*	Added indentation for lego-mode.	Dilip Sequiera	1997-11-18
*	Added some magic commands: proof-frob-locked-end, proof-try-command,	Dilip Sequiera	1997-11-17
*	Includes commented code for Coq version of extent protocol	Healfdene Goguen	1997-11-13
*	Changed pbp-change-goal so that it only "Show"s the goal pointed at.	Healfdene Goguen	1997-11-12
*	Started modifications for emacs19 port.	Dilip Sequiera	1997-11-10
*	Put in a workaround for a strange bug in comint which was finding a bunch	Dilip Sequiera	1997-11-10
*	Parameterize by proof-goal-hyp-fn in pbp-make-top-extent, to handle	Healfdene Goguen	1997-11-06
*	Assign new variable proof-goal-hyp-fn to lego-goal-hyp, which is	Healfdene Goguen	1997-11-06
*	Assign new variable proof-goal-hyp-fn to coq-goal-hyp, which advances	Healfdene Goguen	1997-11-06
*	Updates to Coq fontlock tables	Healfdene Goguen	1997-11-06
*	o implented proof-find-next-terminator available via C-c C-e	Thomas Kleymann	1997-10-31
*	Updates for coq, including:	Healfdene Goguen	1997-10-30
*	Updated comment about extent types	Healfdene Goguen	1997-10-24
*	New indentation for lego-count-undos (smile)	Healfdene Goguen	1997-10-24
*	Fixed coq-count-undos for comments	Healfdene Goguen	1997-10-24
*	Changed order of "Inversion_clear" and "Inversion" so that former is	Healfdene Goguen	1997-10-24
*	Updated proof-segment-up-to to take ""'s into account	Healfdene Goguen	1997-10-22
*	proof-active-terminator inside comment case fixed. Also maybe the	Dilip Sequiera	1997-10-17
*	Fixed coq-shell-prompt-pattern to reflect proof-id	Healfdene Goguen	1997-10-17
*	Added "Induction" as tactic	Healfdene Goguen	1997-10-17
*	fixed a bug in proof-process-active-terminator. Notice that it still	Thomas Kleymann	1997-10-17
*	Figured out display tables.	Dilip Sequiera	1997-10-16
*	Merged Coq changes with main branch.	Dilip Sequiera	1997-10-16
*	Merged Coq changes onto main branch	Dilip Sequiera	1997-10-16
*	merged script management (1.10.2.18) with main branch	Thomas Kleymann	1997-10-16
*	o merged script management (1.20.2.11) on the main branch	Thomas Kleymann	1997-10-16
*	proof-process-active-terminator is now an extension of	Thomas Kleymann	1997-10-14
*	* empty log message *	Thomas Kleymann	1997-10-13
*	put script-management branch back on main branch	Thomas Kleymann	1997-10-13
*	The package pbp is now integrated in the proof package	Thomas Kleymann	1997-10-13
*	lego-count-undos is now aware that comments are treated separately	Thomas Kleymann	1997-10-13
*	* empty log message *	Healfdene Goguen	1997-10-08
*	This commit was generated by cvs2git to track changes on a CVS vendor	David Aspinall	1997-09-18
\|\
\| *	X-Symbol version 4.45 beta	David Aspinall	1997-09-18
* \|	This commit was generated by cvs2git to track changes on a CVS vendor	David Aspinall	1997-09-17
\|\\|
\| *	X-Symbol version 4.45 beta	David Aspinall	1997-09-17
* \|	minor change in font-lock pattern	Thomas Kleymann	1997-08-25
* \|	implementation of pbptop now records if selected goal is not current,	Thomas Kleymann	1997-03-06
* \|	improved highlighting of error messages	Thomas Kleymann	1997-01-27
* \|	support for highlighting Error messages in pbp-mode without using font-lock	Thomas Kleymann	1996-12-12
* \|	removed font-lock support for Error messages; this is now supported in	Thomas Kleymann	1996-12-12
* \|	Took out some debugging code accidentally left in.	Dilip Sequiera	1996-12-09
* \|	Speeded up proof-by-pointing things	Dilip Sequiera	1996-12-09
* \|	added variable pbp-mode-is so that pbp-mode can be inherited	Thomas Kleymann	1996-12-05
* \|	added font-lock properties for pbp-lego-mode	Thomas Kleymann	1996-12-05
* \|	added pbp-mode	Thomas Kleymann	1996-12-03
* \|	Invisible pbp command handling	Dilip Sequiera	1996-12-03