index
:
proof-general
master
Emacs interface for proof assistants
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
coq
Commit message (
Expand
)
Author
Age
*
Adding the option to highlight susual symbols.
Pierre Courtieu
2016-07-22
*
Highlight Existing Class like Existing Instance (#85)
Jason Gross
2016-07-03
*
Highlight [nra] like [nia] and [lia] and [lra] (#84)
Jason Gross
2016-07-01
*
Fix a typo
Clément Pit--Claudel
2016-06-23
*
par-compile: Don't try to compile plugins (cm.*)
Clément Pit--Claudel
2016-06-23
*
Fix a type error hidden until recent emacs.
Pierre Courtieu
2016-06-23
*
Coq: option to prefer top over bottom of concl.
Pierre Courtieu
2016-06-23
*
Color lia, romega, nia, psatz, nsatz, lra
Jason Gross
2016-06-10
*
abbrev twivking.
Pierre Courtieu
2016-06-08
*
Fixing font-locking of unicode forall etc.
Pierre Courtieu
2016-06-08
*
Fixing a smal glitch in indentation.
Pierre Courtieu
2016-05-27
*
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-20
|
*
Fail silently if Coq's version can't be detected
Clément Pit--Claudel
2016-05-19
|
*
Merge branch 'master' of github.com:ProofGeneral/PG
Clément Pit--Claudel
2016-05-16
|
|
\
|
|
/
|
/
|
|
*
Don't offer "" as the default in C-c C-c C-a
Clément Pit--Claudel
2016-05-16
|
*
coq-syntax: Add a debug spec
Clément Pit--Claudel
2016-05-16
*
|
Merge branch 'master' of github.com:ProofGeneral/PG
Pierre Courtieu
2016-05-02
|
\
|
*
|
Fixing detection of symbol at point.
Pierre Courtieu
2016-05-02
|
*
Don't use string-empty-p
Clément Pit--Claudel
2016-04-25
|
*
Respect user settings in coq-insert-intros
Clément Pit--Claudel
2016-04-14
|
/
*
Option to toggle optimising response windo heigth.
Pierre Courtieu
2016-03-21
*
Adding more keywords (Local xxx).
Pierre Courtieu
2016-03-09
*
Fixed #64 again. e2c5da0 commits was wrong.
Pierre Courtieu
2016-03-09
*
Fix #47.
Pierre Courtieu
2016-03-09
*
Fix #64. Use syntax-ppss in fill-nobreak-predicate.
Pierre Courtieu
2016-03-09
*
Fixing a small glitch in indentation.
Pierre Courtieu
2016-03-09
*
Fix #63 (efficiency pb in indentation).
Pierre Courtieu
2016-03-09
*
Fixing #62.
Pierre Courtieu
2016-03-08
*
Avoiding useless computation in indentation code.
Pierre Courtieu
2016-03-08
*
Should fix #49 and #55 (compilation of From .. Require).
Pierre Courtieu
2016-03-08
*
Small fix for -Q options in loadpath.
Pierre Courtieu
2016-03-08
*
Highlight ltac:(), constr:(), and uconstr:()
Clément Pit--Claudel
2016-03-05
*
Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands)
Clément Pit--Claudel
2016-02-29
*
Remove leftover comment
Clément Pit--Claudel
2016-02-28
*
Don't add the ‘Time’ prefix to internal Coq commands
Clément Pit--Claudel
2016-02-28
*
Add uconstr to the (ltac constr) list in SMIE
Clément Pit--Claudel
2016-02-27
*
Fix a typo: s/coq-modulestart-proofstart/coq-indent-proofstart/
Clément Pit--Claudel
2016-02-27
*
Add a :safe predicate to indentation variables
Clément Pit--Claudel
2016-02-27
*
Adding missing keywords
Pierre Courtieu
2016-02-18
*
Merge pull request #40 from hendriktews/proof-tree
Pierre Courtieu
2016-02-17
|
\
*
|
Ensure that version detection does not fail in 24.3
Clément Pit--Claudel
2016-02-06
*
|
Use coq-prog-name to autodetect version number
Clément Pit--Claudel
2016-02-06
*
|
Fixed recent coq syntax change (tac !H become tac (H)).
Pierre Courtieu
2016-01-27
|
*
basic proof tree changes for Coq 8.5
Hendrik Tews
2016-01-24
|
/
*
fix #36.
Pierre Courtieu
2016-01-19
*
Add a few comments to explain values of coq-load-path
Clément Pit--Claudel
2016-01-14
*
Mark coq-load-path-include-current as obsolete
Clément Pit--Claudel
2016-01-14
*
Automatically detect which version of Coq we're using
Clément Pit--Claudel
2016-01-14
*
Refactor the project file parsing code
Clément Pit--Claudel
2016-01-14
[next]