aboutsummaryrefslogtreecommitdiff
path: root/coq/coq-syntax.el
AgeCommit message (Expand)Author
2010-10-10coq-generic-expression: fix this to match symbols, not merely words.David Aspinall
2010-10-01ReFixed bug trac 356.Pierre Courtieu
2010-09-28Fixed colorization bug #356, introduced by a previous fix of bug 140.Pierre Courtieu
2010-09-22Fix bug trac 140 by writing a cleaner regexp than (proof-ids ... " ").Pierre Courtieu
2010-09-22Fix some bugs in coq regexp generationDavid Aspinall
2010-09-22Remove support for Emacs <21 in syntax tableDavid Aspinall
2010-09-09Cleaning indentation code.Pierre Courtieu
2010-09-03Fixed indentation which was broken by a previous commit.Pierre Courtieu
2010-09-03Adding some keywords.Pierre Courtieu
2010-09-03First fix of bug introduced by the last font-lock fix. Not finished.Pierre Courtieu
2010-09-01Fixed bug #346. Coq code was using proof-ids-to-regexp on regexpPierre Courtieu
2010-08-30Fix commentDavid Aspinall
2010-08-30Fix syntax for Local prefix (see Trac #348)David Aspinall
2010-05-17Added a "remember this" window. Experimental.Pierre Courtieu
2009-09-17Added some more syntax keywords. Made admit tactic with its own redPierre Courtieu
2009-09-17Added some syntax keywords thanks to Mathieu Sozeau.Pierre Courtieu
2009-09-10Clean compileDavid Aspinall
2009-09-10Fix compilation for Coq, including requires and some old/renamed settings.David Aspinall
2009-09-08Remove Coq 8.0 codeDavid Aspinall
2009-09-08Remove more of 80 codeDavid Aspinall
2009-09-07Fix compile warnings and ensure compiled code behaves as expected.David Aspinall
2009-09-05Clean whitespaceDavid Aspinall
2009-08-31Made customizable holes mode completion in abbreviations.Pierre Courtieu
2009-08-17Minor changes from Stefan Monnier's patchDavid Aspinall
2008-07-24Merge changes from Version4Branch.David Aspinall
2008-07-21todo added fo coq.Pierre Courtieu
2008-05-20Fixed a bug with coq-prog-name.Pierre Courtieu
2008-04-11Small fix with response buffer scrolling.Pierre Courtieu
2008-03-05fixed syntax table + thing-at-point.Pierre Courtieu
2008-02-01coq:cutomizable bound variable highlight (finally working)Assia Mahboubi
2008-01-31Updated.David Aspinall
2008-01-31Use proof-locate-executable so works out-of-the-box on Windows.David Aspinall
2008-01-31Remove CVS merge junk!David Aspinall
2008-01-31updated CHANGESAssia Mahboubi
2008-01-30coq : sorry, reverting previous buggy customizationAssia Mahboubi
2008-01-30Added a boolean defcustom test to make optional the highlight of variablesAssia Mahboubi
2008-01-30coq : changing highlight of solve, adding ExportAssia Mahboubi
2008-01-28Fixed indentation and goal display.Pierre Courtieu
2008-01-28Fixed a problem with a wrong side effect on syntax databases (whenPierre Courtieu
2008-01-15Many compatibility updates, bug fixes, rearrangements for compilation.David Aspinall
2008-01-03Fixed abbrev installation. + small fixes.Pierre Courtieu
2007-12-14Fix compilation problems and rearrange startup settings for coq-prog-name,coq...David Aspinall
2007-12-14Attempt to fix compile problemsDavid Aspinall
2007-12-14coq-goal-command-str-p: Fix suspected typo shown up by compile warning.David Aspinall
2007-12-12Compatibility with coq trunk where some special symbols are removed.Pierre Courtieu
2007-12-07Print Coercions added to coq-syntaxAssia Mahboubi
2007-12-05Corollary added to Coq startersAssia Mahboubi
2007-11-30coq solve tacs modifiedAssia Mahboubi
2007-11-26colouring for Reserved NotationsAssia Mahboubi
2007-11-20removed 'by'form coq-reserved and added it to coq-solve-tacticsAssia Mahboubi