proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Adding the option to highlight susual symbols.	Pierre Courtieu	2016-07-22
\| \| \| \| \|	This may look ugly to the majority, so I let it off by default. I find it helpfull to have structuring symbols bold.
*	Merge pull request #87 from erikmd/patch-1	Pierre Courtieu	2016-07-20
\|\ \| \| \| \|	Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta)
* \|	Fix inforef references to the emacs manual. (#88)	Yuval Langer	2016-07-07
\| \|
\| *	Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta).	Erik Martin-Dorel	2016-07-04
\|/
*	Highlight Existing Class like Existing Instance (#85)	Jason Gross	2016-07-03
\| \| \|	Closes #81
*	Add Travis CI badge.	Erik Martin-Dorel	2016-07-03
\|
*	emacs-git Travis build: Fix URL of Emacs repo & Build against emacs-25 branch.	Erik Martin-Dorel	2016-07-03
\| \| \| \|	Ref: https://github.com/FStarLang/fstar-mode.el/blob/master/Makefile.travis
*	Update README.md.	Erik Martin-Dorel	2016-07-03
\| \| \| \| \|	- Specify the language for code excerpts - Refactor the "More info" section.
*	Update a link (for latest version of FAQ).	Erik Martin-Dorel	2016-07-03
\|
*	Fix link.	Erik Martin-Dorel	2016-07-03
\|
*	Highlight [nra] like [nia] and [lia] and [lra] (#84)	Jason Gross	2016-07-01
\|
*	Fix a typo	Clément Pit--Claudel	2016-06-23
\|
*	Add myself to list of authors	Clément Pit--Claudel	2016-06-23
\|
*	par-compile: Don't try to compile plugins (cm.*)	Clément Pit--Claudel	2016-06-23
\|
*	Fix a type error hidden until recent emacs.	Pierre Courtieu	2016-06-23
\|
*	Updating CHANGES.	Pierre Courtieu	2016-06-23
\|
*	Coq: option to prefer top over bottom of concl.	Pierre Courtieu	2016-06-23
\|
*	coq-load-path docs: norec -> nonrec (#79)	Timothy Bourke	2016-06-18
\|
*	Reset proof-script-buffer to nil if -ready-prover fails	Clément Pit--Claudel	2016-06-10
\| \| \| \|	Fixes #65
*	Color lia, romega, nia, psatz, nsatz, lra	Jason Gross	2016-06-10
\| \| \| \|	This closes #77
*	abbrev twivking.	Pierre Courtieu	2016-06-08
\|
*	Fixing font-locking of unicode forall etc.	Pierre Courtieu	2016-06-08
\|
*	Merge branch 'master' of github.com:ProofGeneral/PG	Pierre Courtieu	2016-05-27
\|\
* \|	Fixing a smal glitch in indentation.	Pierre Courtieu	2016-05-27
\| \|
\| *	Update license information for new logo	Clément Pit--Claudel	2016-05-25
\| \|
\| *	Update PG's logo	Clément Pit--Claudel	2016-05-24
\|/ \| \| \| \| \| \|	The new art is a contribution of Yoshihiro Imai (http://proofcafe.org/~yoshihiro503/), first released at https://github.com/yoshihiro503/generaltan and kindly made available under the terms of the GPL. Many thanks!
*	Merge branch 'master' of github.com:ProofGeneral/PG	Pierre Courtieu	2016-05-20
\|\
* \|	Fix #72+ make user keywords prioritized over default ones.	Pierre Courtieu	2016-05-20
\| \|
\| *	Fail silently if Coq's version can't be detected	Clément Pit--Claudel	2016-05-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Rationale: if Coq isn't installed, we will detect it when trying to run it, and we don't need to duplicate the error logic. Additionally, change from using process-lines to using shell-command, possibly through file-name-handler. The reason for this change is that we want to do the version detection on the remote server if we're running in Tramp.
\| *	Merge branch 'master' of github.com:ProofGeneral/PG	Clément Pit--Claudel	2016-05-16
\| \|\ \| \|/ \|/\|
\| *	Don't offer "" as the default in C-c C-c C-a	Clément Pit--Claudel	2016-05-16
\| \|
\| *	coq-syntax: Add a debug spec	Clément Pit--Claudel	2016-05-16
\| \|
* \|	Merge branch 'master' of github.com:ProofGeneral/PG	Pierre Courtieu	2016-05-02
\|\\|
* \|	Fixing detection of symbol at point.	Pierre Courtieu	2016-05-02
\| \| \| \| \| \| \| \| \| \| \| \|	Quote at start of a word should not be considered part of the word. Other characters than ' or _ are punctuation.
\| *	Don't use string-empty-p	Clément Pit--Claudel	2016-04-25
\| \| \| \| \| \| \| \|	It's too recent
\| *	Merge pull request #68 from ProofGeneral/67-intros-and-PG-settings	Pierre Courtieu	2016-04-15
\|/\| \| \| \| \|	Respect user settings in coq-insert-intros
\| *	Respect user settings in coq-insert-intros	Clément Pit--Claudel	2016-04-14
\|/ \| \| \|	Fixes #67.
*	updating CHANGES to the last commit.	Pierre Courtieu	2016-03-21
\|
*	Option to toggle optimising response windo heigth.	Pierre Courtieu	2016-03-21
\|
*	Adding more keywords (Local xxx).	Pierre Courtieu	2016-03-09
\|
*	Fixed #64 again. e2c5da0 commits was wrong.	Pierre Courtieu	2016-03-09
\|
*	Fix #47.	Pierre Courtieu	2016-03-09
\| \| \| \|	There are many other issued with coq-smie-forward-token.
*	Fix #64. Use syntax-ppss in fill-nobreak-predicate.	Pierre Courtieu	2016-03-09
\| \| \| \| \|	More robust to font-lock tweaks that change font inside comments (whitespace mode etc).
*	Fixing a small glitch in indentation.	Pierre Courtieu	2016-03-09
\| \| \| \| \|	if a "; tactic" is not at the end of its line, (hanging) then it should not act on indetation of next line.
*	Fix #63 (efficiency pb in indentation).	Pierre Courtieu	2016-03-09
\|
*	Fixing #62.	Pierre Courtieu	2016-03-08
\| \| \| \| \|	I don't know if it is a coq bug that bullet do not support Time. I remove Time from bullets for the moment.
*	Avoiding useless computation in indentation code.	Pierre Courtieu	2016-03-08
\|
*	Should fix #49 and #55 (compilation of From .. Require).	Pierre Courtieu	2016-03-08
\|
*	Small fix for -Q options in loadpath.	Pierre Courtieu	2016-03-08
\|
*	Highlight ltac:(), constr:(), and uconstr:()	Clément Pit--Claudel	2016-03-05
\| \| \| \|	Also refactor coq-font-lock-keywords-1 slightly.