index
:
proof-general
master
Emacs plugins for proof management systems
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
coq
/
coq-syntax.el
Age
Commit message (
Expand
)
Author
2016-05-20
Merge branch 'master' of github.com:ProofGeneral/PG
Pierre Courtieu
2016-05-20
Fix #72+ make user keywords prioritized over default ones.
Pierre Courtieu
2016-05-16
Merge branch 'master' of github.com:ProofGeneral/PG
Clément Pit--Claudel
2016-05-16
coq-syntax: Add a debug spec
Clément Pit--Claudel
2016-05-02
Fixing detection of symbol at point.
Pierre Courtieu
2016-03-09
Adding more keywords (Local xxx).
Pierre Courtieu
2016-03-05
Highlight ltac:(), constr:(), and uconstr:()
Clément Pit--Claudel
2016-02-18
Adding missing keywords
Pierre Courtieu
2016-01-19
fix #36.
Pierre Courtieu
2015-11-23
Introduce a coq-question-mark-face
Clément Pit--Claudel
2015-10-15
Fixed the regexp for colorizing hyps in the goal.
Pierre Courtieu
2015-10-06
Trying to deal with debug mode.
Pierre Courtieu
2015-09-29
colorizing hypothesis in compact mode.
Pierre Courtieu
2015-09-22
hyps highlighting now supports compact contexts (in coq trunk soon).
Pierre Courtieu
2015-05-07
Fixes #492. fixed regexp (\\< --> \\_< everywhere).
Pierre Courtieu
2015-05-07
Fixes #484. Added syntax.
Pierre Courtieu
2015-04-14
bold unicode biders + Fixing highlighting in goals and response buffers + cle...
Pierre Courtieu
2015-04-13
Debugging font-lock for ∀, ∃, and λ.
Pierre Courtieu
2015-04-10
Added unicode forall in font-lock regexps.
Pierre Courtieu
2015-04-07
Fixed coq-id definition to be correct wrt to coq grammar.
Pierre Courtieu
2015-04-07
Fixed highlighting of evars.
Pierre Courtieu
2015-03-27
Fix disable evar colorizing in coq file.
Pierre Courtieu
2015-03-26
Colorizing hyps names robustified. Still incomplete.
Pierre Courtieu
2015-03-26
Fixed a smal bug in colorizing response buffer.
Pierre Courtieu
2015-03-24
fixed gfail hilighting.
Pierre Courtieu
2015-03-24
added some keywords
Pierre Courtieu
2015-03-23
Highlighting evars.
Pierre Courtieu
2015-03-23
Fixed lazymatch and multimatch indentation/highlighting.
Pierre Courtieu
2015-03-13
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-04
Fixed Proof end/start detection on Proof using ...
Pierre Courtieu
2015-02-23
Fixed a bug in syntax table making fontlock and indentation fail.
Pierre Courtieu
2015-02-05
Fix colorization of for coq multiple hypothesis on the same line.
Pierre Courtieu
2015-02-04
Fixed previous commit (wrong regexp).
Pierre Courtieu
2015-02-03
coloring names in resposne and goals
Pierre Courtieu
2015-02-03
beautified a bit error messages.
Pierre Courtieu
2014-06-06
* coq/coq-smie.el: Fix precedence of 'else'.
Stefan Monnier
2013-07-10
Fixing #477. Adding Proposition as a goal-starter keyword.
Pierre Courtieu
2012-07-24
Fixing compilation. Still need to verify some smie stuff on different version...
Pierre Courtieu
2012-06-28
Complete rework of the indentation mechanism using smie. The first
Pierre Courtieu
2012-06-11
Trying to minimize the slowness of indentation when no "Proof." is
Pierre Courtieu
2012-06-06
Trying to fix some minor indentation bugs with infox operators.
Pierre Courtieu
2012-05-31
Fix of a bug. coq id can start with underscore.
Pierre Courtieu
2011-08-23
Move coq-prog-name back to coq.el
David Aspinall
2011-07-29
Fixing track 414 by adding Preterm as a state preserving command.
Pierre Courtieu
2011-06-04
Updated the old code for indentation, in case Stefan cannot finish the
Pierre Courtieu
2011-05-31
Added indentation for BeginSubProof/EndSubProof.
Pierre Courtieu
2011-05-17
Fixed #394. There is a bug with kfont-lock-keywords. The workaround is
Pierre Courtieu
2011-04-15
* fix overwriting setq coq-prog-name before loading Proof General
Hendrik Tews
2011-01-12
Add preliminary support for multiple files for coq.
Hendrik Tews
[prev]
[next]