proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2005-05-31	Document proof-shell-start, proof-shell-exit keys	David Aspinall

2005-05-31	use physical path;	Makarius Wenzel

2005-05-31	tuned;	Makarius Wenzel

2005-05-22	removed find_rwrites, print_intros;	Makarius Wenzel

2005-05-17	Updated.	David Aspinall

2005-05-17	Fix menu path to Customize	David Aspinall

2005-05-17	Set version tag for new release.	David Aspinall

2005-05-17	- Don't just reuse visible frames but also iconified ones.	David Aspinall
	- When proof-three-window-enable is nil, don't mark a dedicated window as non-dedicated. - Don't make the window-size-fixed. It's a real pain in the rear.
2005-05-17	Documentation.	David Aspinall

2005-05-17	Disable Twelf support by default	David Aspinall

2005-05-17	Fix the removal of ".UTF-8" from LANG.	David Aspinall

2005-05-17	Updated.	David Aspinall

2005-05-17	Add missing lib/	David Aspinall

2005-05-17	- shell-command-to-string can fail in various corner cases.	David Aspinall

2005-05-17	- Remove wrong docstring on make-detached-span.	David Aspinall
	- Basically rewrite span-overlay.el to better use the built-in overlay facilities. - Complain about the namespace pollution in span*.el.
2005-05-17	Deleted file	David Aspinall

2005-05-17	Updated.	David Aspinall

2005-05-17	added -L option;	Makarius Wenzel
	tuned;
2005-05-10	undeleted;	Makarius Wenzel

2005-04-27	Add FAQ about favourites	David Aspinall

2005-04-21	added some entris in coq menus.	Pierre Courtieu

2005-04-20	cleaned a bit coq.el (checkdoc). Put some comments to tell what is to	Pierre Courtieu
	be removed when coq-8.0 becomes unsupported.
2005-04-20	New backtracking system for coq continues, this time it uses a new Coq	Pierre Courtieu
	command "Bactrack n m p", where n is the global state label to reach backward, p is the number of aborts and m is an absolute reference to the proof stack to undo (it is the proof stack depth). Coq prompt is now like this: state proof stack num depth __ _ aux < 12 \|aux\|SmallStepAntiReflexive\| 4 < ù ^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^ usual pending proofs usual special char See comments in coq-fin-and-forget-v81.
2005-03-25	Updated.	David Aspinall

2005-03-25	New files.	David Aspinall

2005-03-25	Set version tag for new release.	David Aspinall

2005-03-25	Updated.	David Aspinall

2005-03-25	Remove project todos	David Aspinall

2005-03-25	Remove junk	David Aspinall

2005-03-23	Deleted file	David Aspinall

2005-03-23	Use another symbol	David Aspinall

2005-03-23	Changes from Clemens Ballarin for large X-Symbol fonts	David Aspinall

2005-03-23	New files.	David Aspinall

2005-03-23	Large fonts	David Aspinall

2005-03-21	Updated.	David Aspinall

2005-03-21	Mention Stefan's patches	David Aspinall

2005-03-10	debugging and cleaning of holes.el.	Pierre Courtieu

2005-03-08	small modifications, updating doc string of holes.el.	Pierre Courtieu

2005-03-08	making holes.el cleaner, with the help of Stefan Monnier. I had to	Pierre Courtieu
	adapt coq.el to these modifications.
2005-03-01	cleaning holes.el, starting to making it compatible with skeletons.	Pierre Courtieu

2005-03-01	debugging of holes.el.	Pierre Courtieu

2005-02-21	Debugging holes.el, starting trying to use skeletons.	Pierre Courtieu

2005-02-21	Cleaning file holes.el (tab-width, docstring etc).	Pierre Courtieu

2005-02-17	Updated the doc for new pg/coq. Made modifications advised by Stefan	Pierre Courtieu
	Monnier on holes.el.
2005-02-16	debugging the new holes-mode for fsf emacs. Keyboard shortcuts was	Pierre Courtieu
	badly defined.
2005-02-15	Update FAQ for X-Symbol large fonts (from Clemens Ballarin)	David Aspinall

2005-02-15	Modified holes doc string to fit to new shortcut of holes-mode.	Pierre Courtieu

2005-02-15	Changes from Clemens Ballarin for large X-Symbol fonts	David Aspinall

2005-02-15	New files.	David Aspinall

2005-02-15	Finished making holes.el a real minor-mode. There is a new file	Pierre Courtieu
	holes-load.el which defines the autoloads (enough of them?). All functions have the prefix "holes-", and offending keyboard shortcuts have been either removed or bound to the minor mode. I made holes-mode minor mode automatically turned on in all proof buffers in coq mode (including shell, script and response buffers as it may be useful to copy paste parts of this buffers into holes).