proof-general - Emacs interface for proof assistants

	Commit message (Expand)	Author	Age
*	One needed change for coq included	Healfdene Goguen	1998-01-15
*	o added support for remote proof processes	Thomas Kleymann	1998-01-12
*	improved fume support	Thomas Kleymann	1998-01-05
*	fixed a bug in the indenting functions	Thomas Kleymann	1998-01-05
*	* empty log message *	Thomas Kleymann	1997-12-18
*	o introduced proof-shell-handle-error-hook and bount it by default to	Thomas Kleymann	1997-12-18
*	Noted bug in popup-eager-annotation	Dilip Sequiera	1997-11-26
*	Added C-c C-s to run "Search" in Coq.	Healfdene Goguen	1997-11-26
*	A few new suggestions	Healfdene Goguen	1997-11-26
*	Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1	Healfdene Goguen	1997-11-26
*	o The response buffer focusses on the first goal	Thomas Kleymann	1997-11-26
*	o simplified code:	Thomas Kleymann	1997-11-26
*	simplified code:	Thomas Kleymann	1997-11-26
*	Added proof-execute-minibuffer-cmd and scripting minor mode.	Dilip Sequiera	1997-11-24
*	Added proof-global-p to test whether a 'vanilla should be lifted above	Healfdene Goguen	1997-11-20
*	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