proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Support the Variant vernacular	Tej Chajed	2018-08-17
\| \| \| \| \|	Syntactically looks much like an Inductive, though it is non-recursive so "where" (mutual recursion) is not supported.
*	Fixing last commit.	Pierre Courtieu	2018-06-15
\|
*	Fix #368 (emacs < 25 split-string has no trim arg).	Pierre Courtieu	2018-06-15
\| \| \| \|	Copied some code from company-coq.
*	Fix multiple hyp overlays.	Pierre Courtieu	2018-06-13
\| \| \| \| \|	queries would trigger re-generarion of overlays. Now overlays are generated if there are no overlays already.
*	Fix the fix #355.	Pierre Courtieu	2018-06-13
\| \| \| \|	The fix was bad: no ore hyps were foldable/highlightable.
*	Changed the look of folding/unfolding hyps.	Pierre Courtieu	2018-06-08
\|
*	Small fix in a regexp.	Pierre Courtieu	2018-06-06
\|
*	Shorter CHANGES + smal fixes in hide/highlight hyps code.	Pierre Courtieu	2018-06-04
\|
*	Click hypothesis to (un)hide them.	Pierre Courtieu	2018-06-01
\|
*	Infrastructure for transient hyps highlighting.	Pierre Courtieu	2018-05-31
\|
*	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel	2018-02-21
\|
*	typo in abbrevs.	Pierre Courtieu	2018-02-07
\|
*	Merge pull request #157 from ProofGeneral/elpa	Clément Pit-Claudel	2017-05-05
\|\ \| \| \| \|	[WIP] ELPA/MELPA support
* \|	Typo from commit 758e679e.	Pierre Courtieu	2017-04-25
\| \|
* \|	Preparing new warning tags (no more special chars).	Pierre Courtieu	2017-04-24
\| \|
* \|	Fixing #173.	Pierre Courtieu	2017-03-31
\| \|
* \|	Added support for future new options (trunk).	Pierre Courtieu	2017-03-22
\| \|
\| *	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.
*	Add {Local ,}Axioms like {Local ,}Axiom, fix Parameters (#106)	Jason Gross	2017-01-17
\|
*	Merge pull request #107 from JasonGross/patch-3	hendriktews	2017-01-17
\|\ \| \| \| \|	Add Context to coq-syntax.el
* \|	fix coq-require-command-regexp (fixes #75)	Hendrik Tews	2016-10-28
\| \|
\| *	Add Context to coq-syntax.el	Jason Gross	2016-09-01
\|/
*	Add Reserved Infix like Reserved Notation (#95)	Jason Gross	2016-08-14
\|
*	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.
*	Highlight Existing Class like Existing Instance (#85)	Jason Gross	2016-07-03
\| \| \|	Closes #81
*	Highlight [nra] like [nia] and [lia] and [lra] (#84)	Jason Gross	2016-07-01
\|
*	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
\|
*	Fixing a smal glitch in indentation.	Pierre Courtieu	2016-05-27
\|
*	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
\| \|
\| *	Merge branch 'master' of github.com:ProofGeneral/PG	Clément Pit--Claudel	2016-05-16
\| \|\ \| \|/ \|/\|
\| *	coq-syntax: Add a debug spec	Clément Pit--Claudel	2016-05-16
\| \|
* \|	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.
*	Adding more keywords (Local xxx).	Pierre Courtieu	2016-03-09
\|
*	Highlight ltac:(), constr:(), and uconstr:()	Clément Pit--Claudel	2016-03-05
\| \| \| \|	Also refactor coq-font-lock-keywords-1 slightly.
*	Adding missing keywords	Pierre Courtieu	2016-02-18
\|
*	fix #36.	Pierre Courtieu	2016-01-19
\|
*	Introduce a coq-question-mark-face	Clément Pit--Claudel	2015-11-23
\| \| \| \|	Closes #12
*	Fixed the regexp for colorizing hyps in the goal.	Pierre Courtieu	2015-10-15
\|
*	Trying to deal with debug mode.	Pierre Courtieu	2015-10-06
\|
*	colorizing hypothesis in compact mode.	Pierre Courtieu	2015-09-29
\|
*	hyps highlighting now supports compact contexts (in coq trunk soon).	Pierre Courtieu	2015-09-22
\|
*	Fixes #492. fixed regexp (\\< --> \\_< everywhere).	Pierre Courtieu	2015-05-07
\| \| \| \|	Surprising that this did not raise before...
*	Fixes #484. Added syntax.	Pierre Courtieu	2015-05-07
\|
*	bold unicode biders + Fixing highlighting in goals and response buffers + ↵	Pierre Courtieu	2015-04-14
\| \| \| \|	cleaning.
*	Debugging font-lock for ∀, ∃, and λ.	Pierre Courtieu	2015-04-13
\|
*	Added unicode forall in font-lock regexps.	Pierre Courtieu	2015-04-10
\|
*	Fixed coq-id definition to be correct wrt to coq grammar.	Pierre Courtieu	2015-04-07
\|