proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Some comments for future work.	Pierre Courtieu	2015-03-13
\|
*	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.
*	Customization variables for modules, section and proof indentation.	Pierre Courtieu	2015-03-05
\|
*	Fixed Proof end/start detection on Proof using ...	Pierre Courtieu	2015-03-04
\| \| \| \| \|	Was making scripting confused. P.
*	Fixed compilation issue with previous commit + CHANGE updates.	Pierre Courtieu	2015-03-04
\|
*	Mouse queries.	Pierre Courtieu	2015-03-03
\| \| \| \| \|	If enabled, allows to send queries to coq with (control/shift/control-shift) mouse-1.
*	Coqtop always restarted when switching script buffer.	Pierre Courtieu	2015-03-03
\| \| \| \| \| \|	This comes from Hendrik's compile mode and is actually needed even when this mode is off. When switching scripting buffer, restart the coq shell process, so that it applies local coqtop options.
*	Making freeze buffer hace coq-response-more.	Pierre Courtieu	2015-02-24
\| \| \| \| \|	So that shortcuts work from this buffer. + colorizing.
*	Typo in last commit.	Pierre Courtieu	2015-02-23
\|
*	Fixed a bug in syntax table making fontlock and indentation fail.	Pierre Courtieu	2015-02-23
\| \| \| \|	After some command detecting things at point, the indentation was broken.
*	Fixed read-only error for compile before require option.	Pierre Courtieu	2015-02-11
\| \| \| \| \| \|	the emacs bug seems solved: the error with read-only always occur whatever locale is used. So I toggle read-only off in coq-compile-response.
*	replug removal of induction principle in SearAbout queries.	Pierre Courtieu	2015-02-09
\|
*	Adding function to grab things at point and send queries about it.	Pierre Courtieu	2015-02-09
\| \| \| \|	No shortcut yet but I am testing some "one click" stuff right now.
*	Removed a debugging message.	Pierre Courtieu	2015-02-06
\|
*	Fix colorization of for coq multiple hypothesis on the same line.	Pierre Courtieu	2015-02-05
\|
*	cleaned previous commits (generic variable to disable error coloring).	Pierre Courtieu	2015-02-04
\|
*	Fixed previous commit (wrong regexp).	Pierre Courtieu	2015-02-04
\|
*	coloring names in resposne and goals	Pierre Courtieu	2015-02-03
\|
*	beautified a bit error messages.	Pierre Courtieu	2015-02-03
\|
*	cleaning regexp.	Pierre Courtieu	2015-02-03
\|
*	Set double hit electric terminator back. Disabled by default.	Pierre Courtieu	2015-01-30
\|
*	Fix coq project parsing and interpreting for coq v8.5.	Pierre Courtieu	2015-01-27
\|
*	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
\|
*	failed and commented attempt at improving indentation of records.	Pierre Courtieu	2015-01-09
\|
*	Removing non-smie indentation + fix CHANGES.	Pierre Courtieu	2015-01-09
\|
*	Fixing indentation of pending curly braces.	Pierre Courtieu	2015-01-05
\|
*	Fix compile on 23.x	David Aspinall	2015-01-05
\|
*	trying to indent pending forall in the expected way	Pierre Courtieu	2015-01-05
\|
*	removed debug message.	Pierre Courtieu	2014-12-30
\|
*	fixed indentation (lexing of 'with') + made local coq-load-path.	Pierre Courtieu	2014-12-30
\|
*	fixed a bug in command parsing for coq, due to recent changes.	Pierre Courtieu	2014-12-24
\|
*	typo in indentation cod, found after testing coq/ex/indent.v.	Pierre Courtieu	2014-12-24
\|
*	fixing a small pb in indentation of arrow (->). Not perfect.	Pierre Courtieu	2014-12-24
\|
*	fixed the use of >= 24.4 function string-suffix-p.	Pierre Courtieu	2014-12-24
\|
*	Supporting more bullets (coq 8.5), like ++ or ++++.	Pierre Courtieu	2014-12-23
\|
*	Fix a special case in _CoqProject syntax (empty string).	Pierre Courtieu	2014-12-23
\|
*	Refix prettify compilation bug.	Pierre Courtieu	2014-12-23
\|
*	fixed comilation of prettify setting.	Pierre Courtieu	2014-12-23
\|
*	Fixed a compilation issue + small display glitch in coqpg	Pierre Courtieu	2014-12-22
\|
*	Fixing a bug of multiple frame mode (obsolete variable in emacs > 23.4.	Pierre Courtieu	2014-12-22
\|
*	Fixed response display spurious newlines for coq.	Pierre Courtieu	2014-12-18
\| \| \| \| \| \|	Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly.
*	Remove trailing space in info messages in coq mode.	Pierre Courtieu	2014-12-16
\|
*	Added a way to print eager message without warning face.	Pierre Courtieu	2014-12-16
\| \| \| \| \|	It is the only way I found to display informativemessage appearing before the goal.
*	make name filtering of searchabout more precise.	Pierre Courtieu	2014-12-09
\|
*	Added a variant of searchAbout hiding some spurious entries.	Pierre Courtieu	2014-12-09
\|
*	* coq/coq-smie.el: Fix precedence of 'else'.	Stefan Monnier	2014-06-06
\|
*	* 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 ":=".
*	Rename coq-smie-lexer.el to coq-smie.el.	Stefan Monnier	2014-06-03
\|
*	* coq.el (coq-prettify-symbols-alist): New var.	Stefan Monnier	2014-06-02
\| \| \| \|	(coq-mode-config): Use it.