coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove pointless regex for '""' as the empty string already matches it.	Guillaume Melquiond	2014-09-17
\|
*	Fix highlighting of "Hint Unfold" and "Hint Rewrite".	Guillaume Melquiond	2014-09-17
\|
*	Properly highlight the Export keyword.	Guillaume Melquiond	2014-09-17
\|
*	Fix ambiguous regex in syntax highlighting.	Guillaume Melquiond	2014-09-17
\| \| \| \| \| \| \|	This fix considerably speeds up syntax highlighting. It also avoids burning 100% CPU when typing long identifiers. Finally, identifiers longer than 20 characters are now properly highlighted, since the stack of the automaton no longer overflows because of them.
*	Fix broken syntax highlighting for Coq files using "Proof constr".	Guillaume Melquiond	2014-09-17
\| \| \| \| \| \|	See Eqdep_dec.v for instance. Module declarations were not highlighted because the IDE wrongly believed they were used inside an unterminated proof.
*	Fix broken commit 2bcb2cb.	Guillaume Melquiond	2014-04-28
\|
*	Fix incorrect syntax highlighting after the Goal command.	Guillaume Melquiond	2014-04-28
\|
*	Fix syntax highlighting of "Implicit Arguments" for gtksourceview.	Guillaume Melquiond	2014-03-02
\|
*	Ensure locality modifiers are properly highlighted in CoqIDE.	Guillaume Melquiond	2013-12-03
\|
*	Coqide ported to STM	gareuselesinge	2013-08-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide Fix highlighting of Extraction, Import, Variables	pboutill	2012-09-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Better highlighting of strings in coqide.	aspiwack	2012-08-24
\| \| \| \| \| \| \| \| \| \| \| \|	Strings were not highlighted out of comments. This would lead to funny result, like certain strings (i.e. "(*") to cause all following code to be highlighted as a string. I've added strings in three different contexts (the same where comments are highlighted). I think it's safe to do, I don't know if it's the best way, though. In particular I don't know if it's the best way to highlight notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixes bug #2857.	aspiwack	2012-08-10
\| \| \| \| \| \|	Coqide used the wrong escape sequence to delimit coq phrases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15720 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide highligthing is back (done by gtksourceview).	pboutill	2012-05-02
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15269 85f007b7-540e-0410-9357-904b9bb8a0f7