proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Add coq-Print-Ltac to print an Ltac term	John Grosen	2018-08-07
\|
*	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.
*	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
\|
*	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
\|
*	Infrastructure for transient hyps highlighting.	Pierre Courtieu	2018-05-31
\|
*	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
\|
*	Fix #214.	Pierre Courtieu	2017-12-11
\| \| \| \|	If this works we should probably change the generic function as well.
*	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.
*	Remove mmm and ML4PG contribs and remove references to them in code and docs	Paul Steckler	2017-05-24
\|
*	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
* \|	Preparing new warning tags (no more special chars).	Pierre Courtieu	2017-04-24
\| \|
* \|	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
\| \|
\| *	Remove compile-time calls to proof-ready-for-assistant	Clément Pit--Claudel	2017-03-08
\| \| \| \| \| \| \| \| \| \|	Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el.
\| *	Remove unnecessary calls to 'eval-and-compile'	Clément Pit--Claudel	2017-03-08
\| \|
\| *	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.
*	get threeb frames only when needed	Paul Steckler	2017-03-06
\|
*	one more redundant call removed	Paul Steckler	2017-03-06
\|
*	remove redundant calls, simplify code	Paul Steckler	2017-03-06
\|
*	Refreshing goal when Set Printing xxx. (#162)	Pierre Courtieu	2017-03-03
\| \| \| \| \|	* Close ProofGeneral/PG#161. Issue a "Show" each time a (Uns\|S)et Printing is detected (and a proof is open).
*	Fixing #154.	Pierre Courtieu	2017-02-23
\|
*	save settings not defined with defpacustom (fixes #142)	Hendrik Tews	2017-01-19
\| \| \| \| \| \| \|	- infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual
*	Fix prooftree for Coq 8.6	Hendrik Tews	2017-01-14
\| \| \| \| \| \| \|	In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook.
*	add second argument to looking-back, required in emacs25	Hendrik Tews	2016-12-31
\|
*	properly reset the vio2vo delay timer	Hendrik Tews	2016-12-28
\| \| \| \| \|	cancel-timer does of course not set the variable that holds the timer to nil
*	add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576	Hendrik Tews	2016-12-15
\|
*	fix :get for coq-search-blacklist	Hendrik Tews	2016-12-15
\|
*	Merge pull request #101 from tchajed/print-universes-option	hendriktews	2016-12-15
\|\ \| \| \| \|	Add Set Printing Universes to options menu
* \|	fix customize-group coq	Hendrik Tews	2016-11-30
\| \|
\| *	Add Set Printing Universes to options menu	Tej Chajed	2016-08-15
\|/
*	Replace "Set Implicit Arguments" option with "Set Printing Implicit".	Erik Martin-Dorel	2016-08-14
\| \| \| \|	Closes #99.
*	Coq: option to prefer top over bottom of concl.	Pierre Courtieu	2016-06-23
\|
*	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
\| \|\ \| \|/ \|/\|
\| *	Don't offer "" as the default in C-c C-c C-a	Clément Pit--Claudel	2016-05-16
\| \|
* \|	Merge branch 'master' of github.com:ProofGeneral/PG	Pierre Courtieu	2016-05-02
\|\\|