proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Added a command to send Queries to coq, with completion (C-c C-a C-q).	Pierre Courtieu	2015-03-13
\| \| \| \| \|	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.
*	Added bug fixes in CHANGES.	Pierre Courtieu	2015-03-09
\|
*	Fixed stuff in CHANGES.	Pierre Courtieu	2015-03-05
\|
*	Customization variables for modules, section and proof indentation.	Pierre Courtieu	2015-03-05
\|
*	Fixed compilation issue with previous commit + CHANGE updates.	Pierre Courtieu	2015-03-04
\|
*	coloring names in resposne and goals	Pierre Courtieu	2015-02-03
\|
*	Fixed a bug in script navigation. Updated CHANGE	Pierre Courtieu	2015-01-27
\|
*	changed default indentation of match's cases.	Pierre Courtieu	2015-01-14
\|
*	Removing non-smie indentation + fix CHANGES.	Pierre Courtieu	2015-01-09
\|
*	trying to indent pending forall in the expected way	Pierre Courtieu	2015-01-05
\|
*	Supporting more bullets (coq 8.5), like ++ or ++++.	Pierre Courtieu	2014-12-23
\|
*	* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.	Stefan Monnier	2014-06-04
\| \| \| \| \|	(coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=".
*	Fixing undeclared variables for compilation.	Pierre Courtieu	2013-07-04
\|
*	Added an entry to CHANGEs about coq project fields.	Pierre Courtieu	2013-06-21
\|
*	- implement proof-script insertion	Hendrik Tews	2013-01-21
\|
*	document latest changes	Hendrik Tews	2013-01-17
\|
*	- support bullets and braces in Prooftree	Hendrik Tews	2013-01-15
\| \| \| \|	- prooftree protocol change to version 3
*	write CHANGES	Hendrik Tews	2012-11-15
\|
*	Updates for PG 4.3	David Aspinall	2012-10-19
\|
*	Fixed a bug in three windows mode.	Pierre Courtieu	2012-09-25
\|
*	Added one point + details to CHANGES.	Pierre Courtieu	2012-09-07
\|
*	Fixed double hit terminator. Now it is disabled by default, and	Pierre Courtieu	2012-09-05
\| \| \| \| \| \| \| \|	enabling it disables electric-terminator and vice-versa. In case both are non nil at the same time, then electric teminator has priority. If people like it we may propose this to other modes than coq. + fixed window layout policy.
*	Add user option proof-next-command-insert-space.	David Aspinall	2012-08-14
\|
*	Fixing compilation. Still need to verify some smie stuff on different ↵	Pierre Courtieu	2012-07-24
\| \| \| \|	versions of emacs.
*	Added completion to insert Require, based on coq-load-path.	Pierre Courtieu	2012-07-09
\|
*	updated CHANGES for Coq.	Pierre Courtieu	2012-07-09
\|
*	More fixes in coq indentation.	Pierre Courtieu	2012-07-06
\|
*	Added some detail on the indentation limitation in the CHANGE.	Pierre Courtieu	2012-01-18
\|
*	Fix typo, mention HOL Light	David Aspinall	2012-01-12
\|
*	Add link to Prooftree download	David Aspinall	2012-01-04
\|
*	update CHANGES	Hendrik Tews	2012-01-03
\|
*	Will release 4.2 next, after all	David Aspinall	2011-12-23
\|
*	- protect proof-shell-handle-delayed-output against the case where	Hendrik Tews	2011-12-07
\| \| \| \| \|	proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals
*	Suggest PG 4.1.1 will be released next	David Aspinall	2011-11-15
\|
*	Bump doc version numbers to 4.2pre.	David Aspinall	2011-10-14
\|
*	coq-use-smie not enabled by default	David Aspinall	2011-06-22
\|
*	Ref to Coq chapter in PG manual	David Aspinall	2011-05-16
\|
*	Note recent changes	David Aspinall	2011-01-25
\|
*	Summary: New indentation code using SMIE	Stefan Monnier	2010-11-15
\| \| \| \| \| \| \| \| \| \|	* coq/coq.el (coq-build-prog-args): Avoid meaningless \- escape sequence. (coq-use-smie): New custom var. (coq-smie-grammar): New var. (coq-smie-rules): New function. (coq-guess-or-ask-for-string): Use use-region-p. (coq-mode-config): Use smie-setup if available. * lib/proof-compat.el (use-region-p): Provide fallback definition.
*	Updated.	David Aspinall	2010-11-03
\|
*	Update for config changes.	David Aspinall	2010-10-13
\|
*	proof-use-parser-cache=t default	David Aspinall	2010-10-11
\|
*	Clarify Emacs 22 version	David Aspinall	2010-10-10
\|
*	Support Emacs 23.1+ only.	David Aspinall	2010-10-10
\|
*	Document query identifier	David Aspinall	2010-10-01
\|
*	proof-script-command-separator: removed (always a space)	David Aspinall	2010-10-01
\|
*	Add Document Centred command. Adjust for new menu layout.	David Aspinall	2010-09-21
\|
*	Fixed the cleaning of goals buffer when proof completed	Pierre Courtieu	2010-09-09
\| \| \| \|	+ fixed the refreshing of modeline goal number display.
*	filled CHANGES a bit more precisely.	Pierre Courtieu	2010-09-09
\|
*	Fixed small bugs in indentation.	Pierre Courtieu	2010-09-09
\|