proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Complete rework of the indentation mechanism using smie. The first	Pierre Courtieu	2012-06-28
\| \| \| \| \| \|	version of smie indentation code was a good first try but this one is much faster and cleaner. All desambiguations are done in the lexers, it is still a bit slow on large proofs. Some bugs remain to be fixed.
*	Trying to minimize the slowness of indentation when no "Proof." is	Pierre Courtieu	2012-06-11
\| \| \| \|	given. Seems to work.
*	Trying to fix some minor indentation bugs with infox operators.	Pierre Courtieu	2012-06-06
\|
*	Fix of a bug. coq id can start with underscore.	Pierre Courtieu	2012-05-31
\|
*	Move coq-prog-name back to coq.el	David Aspinall	2011-08-23
\|
*	Fixing track 414 by adding Preterm as a state preserving command.	Pierre Courtieu	2011-07-29
\|
*	Updated the old code for indentation, in case Stefan cannot finish the	Pierre Courtieu	2011-06-04
\| \| \| \| \| \| \|	new one for the release. Added also support for an experimental syntax modification: { .. } is a new syntax for Beginsubproof. ... EndSubproof. There a also few minor behavior changes. The code has changed a lot though.
*	Added indentation for BeginSubProof/EndSubProof.	Pierre Courtieu	2011-05-31
\| \| \| \|	+ added some tactics syntax.
*	Fixed #394. There is a bug with kfont-lock-keywords. The workaround is	Pierre Courtieu	2011-05-17
\| \| \| \|	to change the order in which keywords appear. TO FIX.
*	* fix overwriting setq coq-prog-name before loading Proof General	Hendrik Tews	2011-04-15
\| \| \| \|	* more complete callback listing in proof-action list doc
*	Add preliminary support for multiple files for coq.	Hendrik Tews	2011-01-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The following points are implemented already: - recompile either via an external command (make) or let ProofGeneral handle everything internally - complete dependency tracking and recompilation for coq files in internal mode - support for extending the LoadPath: does almost work, even if specified file-locally - move back to clean state if recompilation fails There are the following known problems: - coq-load-path extensions are not retracted - fails on partially qualified library names
*	coq-generic-expression: fix this to match symbols, not merely words.	David Aspinall	2010-10-10
\| \| \| \|	Otherwise we only see first word of symbols using underscores!
*	ReFixed bug trac 356.	Pierre Courtieu	2010-10-01
\|
*	Fixed colorization bug #356, introduced by a previous fix of bug 140.	Pierre Courtieu	2010-09-28
\|
*	Fix bug trac 140 by writing a cleaner regexp than (proof-ids ... " ").	Pierre Courtieu	2010-09-22
\|
*	Fix some bugs in coq regexp generation	David Aspinall	2010-09-22
\|
*	Remove support for Emacs <21 in syntax table	David Aspinall	2010-09-22
\|
*	Cleaning indentation code.	Pierre Courtieu	2010-09-09
\|
*	Fixed indentation which was broken by a previous commit.	Pierre Courtieu	2010-09-03
\|
*	Adding some keywords.	Pierre Courtieu	2010-09-03
\|
*	First fix of bug introduced by the last font-lock fix. Not finished.	Pierre Courtieu	2010-09-03
\|
*	Fixed bug #346. Coq code was using proof-ids-to-regexp on regexp	Pierre Courtieu	2010-09-01
\| \| \| \|	instead of pure strings.
*	Fix comment	David Aspinall	2010-08-30
\|
*	Fix syntax for Local prefix (see Trac #348)	David Aspinall	2010-08-30
\|
*	Added a "remember this" window. Experimental.	Pierre Courtieu	2010-05-17
\|
*	Added some more syntax keywords. Made admit tactic with its own red	Pierre Courtieu	2009-09-17
\| \| \| \|	culpabilizing face.
*	Added some syntax keywords thanks to Mathieu Sozeau.	Pierre Courtieu	2009-09-17
\|
*	Clean compile	David Aspinall	2009-09-10
\|
*	Fix compilation for Coq, including requires and some old/renamed settings.	David Aspinall	2009-09-10
\|
*	Remove Coq 8.0 code	David Aspinall	2009-09-08
\|
*	Remove more of 80 code	David Aspinall	2009-09-08
\|
*	Fix compile warnings and ensure compiled code behaves as expected.	David Aspinall	2009-09-07
\|
*	Clean whitespace	David Aspinall	2009-09-05
\|
*	Made customizable holes mode completion in abbreviations.	Pierre Courtieu	2009-08-31
\|
*	Minor changes from Stefan Monnier's patch	David Aspinall	2009-08-17
\|
*	Merge changes from Version4Branch.	David Aspinall	2008-07-24
\|
*	todo added fo coq.	Pierre Courtieu	2008-07-21
\|
*	Fixed a bug with coq-prog-name.	Pierre Courtieu	2008-05-20
\|
*	Small fix with response buffer scrolling.	Pierre Courtieu	2008-04-11
\| \| \| \|	+ starting the "insert as" feature.
*	fixed syntax table + thing-at-point.	Pierre Courtieu	2008-03-05
\|
*	coq:cutomizable bound variable highlight (finally working)	Assia Mahboubi	2008-02-01
\|
*	Updated.	David Aspinall	2008-01-31
\|
*	Use proof-locate-executable so works out-of-the-box on Windows.	David Aspinall	2008-01-31
\|
*	Remove CVS merge junk!	David Aspinall	2008-01-31
\|
*	updated CHANGES	Assia Mahboubi	2008-01-31
\| \| \| \|	added an example file in coq/
*	coq : sorry, reverting previous buggy customization	Assia Mahboubi	2008-01-30
\|
*	Added a boolean defcustom test to make optional the highlight of variables	Assia Mahboubi	2008-01-30
\|
*	coq : changing highlight of solve, adding Export	Assia Mahboubi	2008-01-30
\|
*	Fixed indentation and goal display.	Pierre Courtieu	2008-01-28
\|
*	Fixed a problem with a wrong side effect on syntax databases (when	Pierre Courtieu	2008-01-28
\| \| \| \|	sorting for menus).