proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	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
\|
*	Fixed highlighting of evars.	Pierre Courtieu	2015-04-07
\|
*	Fix disable evar colorizing in coq file.	Pierre Courtieu	2015-03-27
\|
*	Colorizing hyps names robustified. Still incomplete.	Pierre Courtieu	2015-03-26
\|
*	Fixed a smal bug in colorizing response buffer.	Pierre Courtieu	2015-03-26
\| \| \| \| \| \|	First constructor of an inductive was colorized as a hyp name. Hyp name colorizing should be done another way. Using font-lock here is probably bad.
*	fixed gfail hilighting.	Pierre Courtieu	2015-03-24
\|
*	added some keywords	Pierre Courtieu	2015-03-24
\|
*	Highlighting evars.	Pierre Courtieu	2015-03-23
\|
*	Fixed lazymatch and multimatch indentation/highlighting.	Pierre Courtieu	2015-03-23
\|
*	Some comments for future work.	Pierre Courtieu	2015-03-13
\|
*	Added a command to send Queries to coq, with completion (C-c C-a C-q).	Pierre Courtieu	2015-03-13
\| \| \| \| \|	Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag.
*	Fixed Proof end/start detection on Proof using ...	Pierre Courtieu	2015-03-04
\| \| \| \| \|	Was making scripting confused. P.
*	Fixed a bug in syntax table making fontlock and indentation fail.	Pierre Courtieu	2015-02-23
\| \| \| \|	After some command detecting things at point, the indentation was broken.
*	Fix colorization of for coq multiple hypothesis on the same line.	Pierre Courtieu	2015-02-05
\|
*	Fixed previous commit (wrong regexp).	Pierre Courtieu	2015-02-04
\|
*	coloring names in resposne and goals	Pierre Courtieu	2015-02-03
\|
*	beautified a bit error messages.	Pierre Courtieu	2015-02-03
\|
*	* coq/coq-smie.el: Fix precedence of 'else'.	Stefan Monnier	2014-06-06
\|
*	Fixing #477. Adding Proposition as a goal-starter keyword.	Pierre Courtieu	2013-07-10
\|
*	Fixing compilation. Still need to verify some smie stuff on different ↵	Pierre Courtieu	2012-07-24
\| \| \| \|	versions of emacs.
*	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.