proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel	2018-02-21
\|
*	Remove mmm and ML4PG contribs and remove references to them in code and docs	Paul Steckler	2017-05-24
\|
*	Fix incorrect uses of defvar	Clément Pit--Claudel	2017-03-08
\| \| \| \| \| \| \|	It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance.
*	(fixes last commit) Added a command to send Queries to coq, with completion ↵	Pierre Courtieu	2015-03-13
\| \| \| \| \| \| \|	(C-c C-a C-q). Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag.
*	Small fix in holes code.	Pierre Courtieu	2012-09-19
\|
*	Summary: Don't quote lambda expressions	Stefan Monnier	2012-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* coq/coq-indent.el (coq-indent-inner-regexp): Remove old X-Symbol element. (coq-save-count, coq-proof-count): * obsolete/plastic/plastic.el (plastic-shell-handle-output): * lib/texi-docstring-magic.el (texi-docstring-magic-insert-magic): * lib/pg-dev.el (emacs-lisp-mode-hook): * lib/maths-menu.el (maths-menu-filter-predicate) (maths-menu-tokenise-insert): * lib/holes.el (holes-next): * lego/lego.el (lego-shell-handle-output): * isar/isabelle-system.el (isabelle-docs-menu): * coq/coq.el (coq-compile-command, coq-compile-auto-save) (coq-compile-ignored-directories, coq-load-path-safep) (proof-shell-handle-delayed-output-hook): Don't quote lambda.
*	Rearrange for scoping	David Aspinall	2009-09-06
\|
*	Add menu moved from Coq menu. Make deactivating holes-mode forget all holes.	David Aspinall	2009-09-06
\|
*	Make holes-abbrev-complete obey status of minor mode.	David Aspinall	2009-09-06
\|
*	Cleanup code and use define-minor-mode.	David Aspinall	2009-09-06
\|
*	Tidy whitespace	David Aspinall	2009-09-05
\|
*	Made indentation optional when replaing # by holes.	Pierre Courtieu	2009-01-14
\|
*	Fixing parenthesis not accepted by recent emacs anymore. fix by Stefan	Pierre Courtieu	2008-10-22
\| \| \| \|	Monnier.
*	Merge changes from Version4Branch.	David Aspinall	2008-07-24
\|
*	Changed the main menu of coq. Changed a shortcut for holes.	Pierre Courtieu	2008-07-21
\|
*	Fix RCS tags	David Aspinall	2008-01-30
\|
*	Don't give error when loaded during "make doc" with old emacs version	David Aspinall	2008-01-28
\|
*	Many compatibility updates, bug fixes, rearrangements for compilation.	David Aspinall	2008-01-15
\|
*	Fixed abbrev installation. + small fixes.	Pierre Courtieu	2008-01-03
\|
*	holes-skeleton-end-hook: no action if mmm-inside-insert-by-key bound	David Aspinall	2007-12-13
\|
*	Started the coq-insert-tactic.	Pierre Courtieu	2006-08-21
\|
*	commit of a small patch from Stefan Monnier, to fix a small bug of	Pierre Courtieu	2006-01-10
\| \| \| \|	drag-mouse-region with holes.
*	debugging and cleaning of holes.el.	Pierre Courtieu	2005-03-10
\|
*	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	2005-03-08
\| \| \| \|	adapt coq.el to these modifications.
*	cleaning holes.el, starting to making it compatible with skeletons.	Pierre Courtieu	2005-03-01
\|
*	debugging of holes.el.	Pierre Courtieu	2005-03-01
\|
*	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-21
\|
*	Updated the doc for new pg/coq. Made modifications advised by Stefan	Pierre Courtieu	2005-02-17
\| \| \| \|	Monnier on holes.el.
*	debugging the new holes-mode for fsf emacs. Keyboard shortcuts was	Pierre Courtieu	2005-02-16
\| \| \| \|	badly defined.
*	Modified holes doc string to fit to new shortcut of holes-mode.	Pierre Courtieu	2005-02-15
\|
*	Finished making holes.el a real minor-mode. There is a new file	Pierre Courtieu	2005-02-15
\| \| \| \| \| \| \| \| \|	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).
*	cleaning holes.el. All functions are prefixed with "holes-". Also	Pierre Courtieu	2005-02-14
\| \| \| \|	modified coq.el and coq-abbrev.el accordingly.
*	Starting to clean holes.el following Stefan Monnier's advices. Making	Pierre Courtieu	2005-02-14
\| \| \| \|	holes a real minor-mode.
*	Renamed file	David Aspinall	2004-08-25