proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Merge pull request #379 from tchajed/variant-keyword	Clément Pit-Claudel	2018-08-21
\|\ \| \| \| \|	Support the Variant vernacular
* \	Merge branch 'master' of github.com:ProofGeneral/PG	Pierre Courtieu	2018-08-18
\|\ \
* \| \|	Fix #7980, keep option order unchanged.	Pierre Courtieu	2018-08-18
\| \| \|
\| \| *	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.
\| *	Add coq-Print-Ltac to print an Ltac term	John Grosen	2018-08-07
\|/
*	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.
*	small fix on hyp overlays.	Pierre Courtieu	2018-06-13
\|
*	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.
*	Small bug unhighlighting.	Pierre Courtieu	2018-06-11
\| \| \| \| \|	Selecting the unhighlightied hyps showed a different region color. Setting the face to nil is better.
*	fix #355 + probable bug.	Pierre Courtieu	2018-06-11
\| \| \| \| \|	By renaming the arg load-path into loadpath I notice that a coq-load-path was used instead of it.
*	key maps + small glitch hyp highlight/folding code.	Pierre Courtieu	2018-06-11
\|
*	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
\|
*	Fixed a typo in previous commits.	Pierre Courtieu	2018-06-01
\|
*	Infrastructure for hypothesis hiding.	Pierre Courtieu	2018-05-31
\|
*	Fixing infrastructure for hypothesis highlighting.	Pierre Courtieu	2018-05-31
\|
*	Merge branch 'master' of github.com:ProofGeneral/PG	Pierre Courtieu	2018-05-31
\|\
* \|	Infrastructure for transient hyps highlighting.	Pierre Courtieu	2018-05-31
\| \|
\| *	small fix of face `coq-symbol-face'	stardiviner	2018-04-22
\| \|
\| *	Merge pull request #207 from SkySkimmer/master	Erik Martin-Dorel	2018-04-08
\|/\| \| \| \| \|	Make coq-prog-args safe when list of strings.
* \|	Fix typos in custom variable descriptions. (#236)	Tej Chajed	2018-03-03
\| \|
* \|	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel	2018-02-21
\| \|
* \|	typo in abbrevs.	Pierre Courtieu	2018-02-07
\| \|
* \|	look for vernac controls before focus bracket, fix for #223	Paul Steckler	2018-01-26
\| \|
* \|	Experimental fix for #220.	Pierre Courtieu	2018-01-15
\| \|
\| *	Make coq-prog-args safe when list of strings.	Gaëtan Gilbert	2017-12-22
\| \| \| \| \| \| \| \|	They could be passed through _CoqProject regardless.
* \|	Fix #214.	Pierre Courtieu	2017-12-11
\| \| \| \| \| \| \| \|	If this works we should probably change the generic function as well.
* \|	Prettier cheat face (background + box).	Pierre Courtieu	2017-11-06
\| \|
* \|	Fix #135.	Pierre Courtieu	2017-11-06
\| \|
* \|	Limited extensibility of smie token detection.	Pierre Courtieu	2017-10-26
\|/
*	changed -emacs-U flag to -emacs	Paul Steckler	2017-07-19
\|
*	Fixing a bug with Set/Unset commands due to recent commits.	Pierre Courtieu	2017-06-08
\| \| \| \| \|	The "Show" inserted now and then would hide the result of Set/Unset commands.
*	Adding a Set Silent + Show when backtracking into a proof.	Pierre Courtieu	2017-06-06
\| \| \| \| \|	Checking whether the backtrack is inside a proof or not is a bit convoluted but seems ok.
*	Merge pull request #185 from psteckler/remove-contribs	psteckler	2017-05-25
\|\ \| \| \| \|	Remove mmm and ML4PG contribs
\| *	Remove mmm and ML4PG contribs and remove references to them in code and docs	Paul Steckler	2017-05-24
\| \|
* \|	Fixing #183.	Pierre Courtieu	2017-05-23
\|/
*	Fixing Set/Unset Printing broken by auto "Show".	Pierre Courtieu	2017-05-16
\| \| \| \| \| \|	Current coq trunk has a bug with Show that I reported (there is a spurious Show executed) which makes C-u C-c C-a C-s fail for now. Should be fixed shortly.
*	temporary fix of automatic intros.	Pierre Courtieu	2017-05-12
\|
*	Change (eval-when (compile) ...) to (eval-when-compile ...)	Clément Pit--Claudel	2017-05-05
\| \| \| \|	This fixes a bunch of compilation warnings
*	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
\| \|
* \|	Fix #176.	Pierre Courtieu	2017-04-19
\| \| \| \| \| \| \| \| \| \|	The code uses several token searcher and the wrong one was called somewhere.
* \|	Fixing #173.	Pierre Courtieu	2017-03-31
\| \|
* \|	Added support for future new options (trunk).	Pierre Courtieu	2017-03-22
\| \|
\| *	Add a FIXME in coq.el	Clément Pit--Claudel	2017-03-08
\| \|