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
*
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
*
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
*
Fix #29 + indentation glitch + regexp refactoring.
Pierre Courtieu
2016-01-14
*
Fixing indentation of ";".
Pierre Courtieu
2016-01-08
*
indentation of ";" more accurate.
Pierre Courtieu
2016-01-08
*
Fixing outdenting in ";" indetation.
Pierre Courtieu
2016-01-08
*
Trying to indent ";" differently inside Ltac defs.
Pierre Courtieu
2016-01-08
*
Fixed indentation of ";" tactical.
Pierre Courtieu
2016-01-07
*
Merge pull request #22 from ProofGeneral/fix-scrolling-buffers
Pierre Courtieu
2016-01-06
|
\
*
|
Adding uset preference coq-indent-semicolon-tactical.
Pierre Courtieu
2016-01-06
*
|
Fixing #25.
Pierre Courtieu
2016-01-06
*
|
Fixing #20. #19 fixed by a commit in coq-8.5.
Pierre Courtieu
2016-01-06
*
|
First try to fix #19 and #20. Not finished.
Pierre Courtieu
2016-01-04
|
*
Fix spurious scrolling of *goals* and *response* buffers
Clément Pit--Claudel
2015-12-31
*
|
comment and readme.
Pierre Courtieu
2015-12-31
*
|
Refactoring. New file coq-system.el.
Pierre Courtieu
2015-12-14
|
/
*
Small refactoring of coqxxx args detection.
Pierre Courtieu
2015-12-14
*
Fixing coq-prog-arg for auto compilation.
Pierre Courtieu
2015-12-14
*
Fixing variable declaration.
Pierre Courtieu
2015-12-10
*
Adding an setting for Search Blacklist coq option.
Pierre Courtieu
2015-12-09
*
Speeding up indentation (regexp optim).
Pierre Courtieu
2015-12-07
*
Speeding up indentation.
Pierre Courtieu
2015-12-07
*
Fixed #15 + more speedup of indentation.
Pierre Courtieu
2015-12-05
*
Fixed a typo.
Pierre Courtieu
2015-12-04
*
Speeding up indentation code (smie lexer).
Pierre Courtieu
2015-11-30
*
A shortcut for coq-insert-as-in-next-command.
Pierre Courtieu
2015-11-26
*
Introduce a coq-question-mark-face
Clément Pit--Claudel
2015-11-23
*
recompilation: Improve error checking
Clément Pit--Claudel
2015-11-17
*
compilation fix (coq-pre-v85).
Pierre Courtieu
2015-11-13
*
Experimenting less brutal frame deletion.
Pierre Courtieu
2015-11-13
*
Fixed auto-width setting not initialized (trac #456).
Pierre Courtieu
2015-11-13
*
Cleaning code for auto width adapting.
Pierre Courtieu
2015-11-13
*
Tentative fix for #10
Clément Pit--Claudel
2015-11-12
*
Debuging: display a warning.
Pierre Courtieu
2015-11-12
*
coq-pre-v85 option to fix coqdep invocation in [compile before require].
Pierre Courtieu
2015-11-02
*
Re-thinking auto-insert-as.
Pierre Courtieu
2015-10-20
*
Fixed the regexp for colorizing hyps in the goal.
Pierre Courtieu
2015-10-15
*
Fixed coq-id-at-point.
Pierre Courtieu
2015-10-13
*
proof-retract-command-hook added + more auto adjust width in coq mode.
Pierre Courtieu
2015-10-13
*
proof-assert-command-hook added + Auto adjust width in coq mode.
Pierre Courtieu
2015-10-12
*
Fixing < 25 use of window-frame (mandatory arg).
Pierre Courtieu
2015-10-09
*
Put 'delete-selection t on coq-terminator-insert
Clément Pit--Claudel
2015-10-06
*
Trying to deal with debug mode.
Pierre Courtieu
2015-10-06
*
colorizing hypothesis in compact mode.
Pierre Courtieu
2015-09-29
[next]