aboutsummaryrefslogtreecommitdiff
path: root/coq/coq-syntax.el
AgeCommit message (Expand)Author
2012-07-24Fixing compilation. Still need to verify some smie stuff on different version...Pierre Courtieu
2012-06-28Complete rework of the indentation mechanism using smie. The firstPierre Courtieu
2012-06-11Trying to minimize the slowness of indentation when no "Proof." isPierre Courtieu
2012-06-06Trying to fix some minor indentation bugs with infox operators.Pierre Courtieu
2012-05-31Fix of a bug. coq id can start with underscore.Pierre Courtieu
2011-08-23Move coq-prog-name back to coq.elDavid Aspinall
2011-07-29Fixing track 414 by adding Preterm as a state preserving command.Pierre Courtieu
2011-06-04Updated the old code for indentation, in case Stefan cannot finish thePierre Courtieu
2011-05-31Added indentation for BeginSubProof/EndSubProof.Pierre Courtieu
2011-05-17Fixed #394. There is a bug with kfont-lock-keywords. The workaround isPierre Courtieu
2011-04-15* fix overwriting setq coq-prog-name before loading Proof GeneralHendrik Tews
2011-01-12Add preliminary support for multiple files for coq.Hendrik Tews
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 15:04:33 +0000