proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Use `cl-lib` instead of `cl` everywhere	Stefan Monnier	2018-12-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Use lexical-binding in a few files where it was easy. Don't require `proof-compat` when it's not used. * coq/coq-db.el: Use lexical-binding. * coq/coq-system.el: Use lexical-binding. (coq--extract-prog-args): Use concatenated-args rather than recomputing it. * coq/coq.el: Require `span` to silence some warnings. * generic/pg-user.el: Use lexical-binding. (complete, add-completion, completion-min-length): Silence warnings. * generic/pg-xml.el: Use lexical-binding. (pg-xml-string-of): Prefer mapconcat to reduce+concat. * generic/proof-depends.el: Use lexical-binding. (proof-dep-split-deps): Use `push`. * generic/proof-shell.el: Require `span` to silence some warnings. (proof-shell-invisible-command): Don't use lexical-let just to build a wasteful η-redex! * lib/holes.el: Use lexical-binding. Remove redundant :group args. * lib/span.el: Use lexical-binding. (span-read-only-hook): Use user-error. (span-raise): Remove, unused.
*	Fix most doc issues raised by (checkdoc)	Erik Martin-Dorel	2018-08-23
\|
*	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel	2018-02-21
\|
*	Change (eval-when (compile) ...) to (eval-when-compile ...)	Clément Pit--Claudel	2017-05-05
\| \| \| \|	This fixes a bunch of compilation warnings
*	Fix prooftree for Coq 8.6	Hendrik Tews	2017-01-14
\| \| \| \| \| \| \|	In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook.
*	fix prooftree crash with long evar lines	Hendrik Tews	2016-12-28
\|
*	- implement proof-script insertion	Hendrik Tews	2013-01-21
\|
*	- implement retract from prooftree	Hendrik Tews	2013-01-20
\|
*	- support Grab Existential Variables for Prooftree	Hendrik Tews	2013-01-17
\| \| \| \|	- protocol change, but stay at version 3
*	- support bullets and braces in Prooftree	Hendrik Tews	2013-01-15
\| \| \| \|	- prooftree protocol change to version 3
*	treat #450 by requiring that proofs are started with Proof	Hendrik Tews	2012-09-12
\|
*	Typo	David Aspinall	2012-01-19
\|
*	* fix case where some existential is instantiated with the last proof command	Hendrik Tews	2012-01-04
\| \| \| \| \| \|	* protocol change - rename proof-complete into proof-finished and add existential info - add proof-complete message
*	merge ProofTreeBranch into main trunk:	Hendrik Tews	2012-01-03
	- add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof