proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	GPL, 3.4 dates	David Aspinall	2002-06-21
\|
*	GPL	David Aspinall	2002-06-21
\|
*	Isar is default over isa.	David Aspinall	2002-06-21
\|
*	GPL	David Aspinall	2002-06-21
\|
*	Mention looping GNU	David Aspinall	2002-06-21
\|
*	Updated.	David Aspinall	2002-06-20
\|
*	Set version tag for new release.	David Aspinall	2002-06-20
\|
*	Updated the doc and the CHANGES file about new backtracking for Coq.	Pierre Courtieu	2002-06-19
\|
*	Match FSF C-button3 binding with XEmacs one	David Aspinall	2002-06-19
\|
*	Doc improvements	David Aspinall	2002-06-19
\|
*	Finished updating the commands and tactic lists of coq-syntax.el.	Pierre Courtieu	2002-06-19
\|
*	updated the lists of commands and tactics in coq-syntax.el.	Pierre Courtieu	2002-06-19
\|
*	Use coq-proof-mode-p instead of nesting depth test. Attempt to track ↵	David Aspinall	2002-06-19
\| \| \| \|	nesting depth (fails).
*	Add nested section example to increase the horror.	David Aspinall	2002-06-19
\|
*	Added End for sections, and silly test	David Aspinall	2002-06-19
\|
*	Updated with more notes	David Aspinall	2002-06-19
\|
*	Clean up: remove count-undos, comments, tweak coq-proof-mode-p.	David Aspinall	2002-06-19
\|
*	Updated.	David Aspinall	2002-06-19
\|
*	Add proof-shell-last-prompt.	David Aspinall	2002-06-19
\|
*	Add doc of proof-shell-last-prompt.	David Aspinall	2002-06-19
\|
*	Fix info	David Aspinall	2002-06-19
\|
*	Set version tag for new release.	David Aspinall	2002-06-19
\|
*	Update Emacs versions	David Aspinall	2002-06-18
\|
*	Add news for PG 3.4	David Aspinall	2002-06-18
\|
*	Update magic. Document nested proof settings.	David Aspinall	2002-06-18
\|
*	Removed lift-global stuff. coq-find-and-forget: only undo undoable tactics.	David Aspinall	2002-06-18
\|
*	Remove lift-global function.	David Aspinall	2002-06-18
\|
*	Remove global testing and lift-global function; rename proof-nested-goals -> ↵	David Aspinall	2002-06-18
\| \| \| \|	proof-nested-goals-history.
*	Added some non-undoable tactics	David Aspinall	2002-06-18
\|
*	Added some sections	David Aspinall	2002-06-18
\|
*	News item for PG 3.4	David Aspinall	2002-06-18
\|
*	Added the backtrack mechanism for sections. Seems to work.	Pierre Courtieu	2002-06-18
\|
*	Added a function to inspect the prompt of Coq, in order to know if we	Pierre Courtieu	2002-06-18
\| \| \| \|	are in proof-mode. Redundant with proof-nesting-depth.
*	Attempt at (alledgedly) more robust solution to find-and-forget.	David Aspinall	2002-06-18
\|
*	Fix	David Aspinall	2002-06-18
\|
*	Add more declarations	David Aspinall	2002-06-18
\|
*	Test using proof-nesting-depth before calling Reset	David Aspinall	2002-06-18
\|
*	Minor changes.	Pierre Courtieu	2002-06-14
\|
*	Print and Check guess their argument from the region or the string	Pierre Courtieu	2002-06-14
\| \| \| \|	near the point.
*	Disable count-undos function, just use find-and-forget.	David Aspinall	2002-06-13
\|
*	A nil setting of proof-kill-goal-command forces use of proof-find-and-forget ↵	David Aspinall	2002-06-13
\| \| \| \|	for all retraction.
*	Docs	David Aspinall	2002-06-13
\|
*	Experiment with showing real prover output for aborted proofs.	David Aspinall	2002-06-13
\|
*	Revised find-and-forget function, which also works for count-undos.	David Aspinall	2002-06-12
\|
*	More test cases, summary of situation.	David Aspinall	2002-06-12
\|
*	Second variant of next-span, without doubly nested loop	David Aspinall	2002-06-12
\|
*	Improve imp of next-span	David Aspinall	2002-06-12
\|
*	Note of another bug	David Aspinall	2002-06-12
\|
*	Test for find-and-forget using Back always instead of Reset.	David Aspinall	2002-06-12
\|
*	Add test t4 for extra depth of nesting	David Aspinall	2002-06-12
\|