aboutsummaryrefslogtreecommitdiff
path: root/coq/coq-syntax.el
AgeCommit message (Expand)Author
2016-05-20Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2016-05-20Fix #72+ make user keywords prioritized over default ones.Pierre Courtieu
2016-05-16Merge branch 'master' of github.com:ProofGeneral/PGClément Pit--Claudel
2016-05-16coq-syntax: Add a debug specClément Pit--Claudel
2016-05-02Fixing detection of symbol at point.Pierre Courtieu
2016-03-09Adding more keywords (Local xxx).Pierre Courtieu
2016-03-05Highlight ltac:(), constr:(), and uconstr:()Clément Pit--Claudel
2016-02-18Adding missing keywordsPierre Courtieu
2016-01-19fix #36.Pierre Courtieu
2015-11-23Introduce a coq-question-mark-faceClément Pit--Claudel
2015-10-15Fixed the regexp for colorizing hyps in the goal.Pierre Courtieu
2015-10-06Trying to deal with debug mode.Pierre Courtieu
2015-09-29colorizing hypothesis in compact mode.Pierre Courtieu
2015-09-22hyps highlighting now supports compact contexts (in coq trunk soon).Pierre Courtieu
2015-05-07Fixes #492. fixed regexp (\\< --> \\_< everywhere).Pierre Courtieu
2015-05-07Fixes #484. Added syntax.Pierre Courtieu
2015-04-14bold unicode biders + Fixing highlighting in goals and response buffers + cle...Pierre Courtieu
2015-04-13Debugging font-lock for ∀, ∃, and λ.Pierre Courtieu
2015-04-10Added unicode forall in font-lock regexps.Pierre Courtieu
2015-04-07Fixed coq-id definition to be correct wrt to coq grammar.Pierre Courtieu
2015-04-07Fixed highlighting of evars.Pierre Courtieu
2015-03-27Fix disable evar colorizing in coq file.Pierre Courtieu
2015-03-26Colorizing hyps names robustified. Still incomplete.Pierre Courtieu
2015-03-26Fixed a smal bug in colorizing response buffer.Pierre Courtieu
2015-03-24fixed gfail hilighting.Pierre Courtieu
2015-03-24added some keywordsPierre Courtieu
2015-03-23Highlighting evars.Pierre Courtieu
2015-03-23Fixed lazymatch and multimatch indentation/highlighting.Pierre Courtieu
2015-03-13Some comments for future work.Pierre Courtieu
2015-03-13Added a command to send Queries to coq, with completion (C-c C-a C-q).Pierre Courtieu
2015-03-04Fixed Proof end/start detection on Proof using ...Pierre Courtieu
2015-02-23Fixed a bug in syntax table making fontlock and indentation fail.Pierre Courtieu
2015-02-05Fix colorization of for coq multiple hypothesis on the same line.Pierre Courtieu
2015-02-04Fixed previous commit (wrong regexp).Pierre Courtieu
2015-02-03coloring names in resposne and goalsPierre Courtieu
2015-02-03beautified a bit error messages.Pierre Courtieu
2014-06-06* coq/coq-smie.el: Fix precedence of 'else'.Stefan Monnier
2013-07-10Fixing #477. Adding Proposition as a goal-starter keyword.Pierre Courtieu
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