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.el
Age
Commit message (
Expand
)
Author
2011-01-19
- switch off automatic compilation for coq to not surprise users
Hendrik Tews
2011-01-18
- fixed stale load path problem with killing the proof shell in
Hendrik Tews
2011-01-18
- implemented coq-lock-ancestors as described in the docs already
Hendrik Tews
2011-01-18
Localise compilation fix for dynamic scope of `queueitems\'.
David Aspinall
2011-01-18
- fixed compilation errors
Hendrik Tews
2011-01-18
- fix broken external compilation
Hendrik Tews
2011-01-17
fix problems in test cases
Hendrik Tews
2011-01-14
- more coq test cases (some with surprising and embarrassing bugs)
Hendrik Tews
2011-01-14
- simple backward compatible change to invoke a function to
Hendrik Tews
2011-01-14
- Remove nonfunctional Add LoadPath code.
Hendrik Tews
2011-01-12
Add preliminary support for multiple files for coq.
Hendrik Tews
2010-11-25
Fix compile problem with smie code on Emacs <=23.3
David Aspinall
2010-11-15
Summary: New indentation code using SMIE
Stefan Monnier
2010-10-22
Fixed a bug with utf8 error highlighting in coq 8.3 (bugs with 8.2
Pierre Courtieu
2010-10-10
coq-find-and-forget: Allow undoing prover processed regions
David Aspinall
2010-10-04
Fixes in strings/comments from Erik Martin-Dorel
David Aspinall
2010-10-04
coq-insert-solve-tactic: added (credit:Erik Martin-Dorel, patch from trac #35...
David Aspinall
2010-10-01
Rename span-add-self-removing-span
David Aspinall
2010-10-01
coq-highlight-error: use span-add-self-removing-span (highlight and removal i...
David Aspinall
2010-10-01
coq-allow-highlight-error: remove this setting, now proof-shell-error-or-inte...
David Aspinall
2010-10-01
Add key binding fixes from Erik Martin-Dorel (see Trac#359).
David Aspinall
2010-09-28
Fixed redundant undo limit custom variables.
Pierre Courtieu
2010-09-09
Revert last change, version from Pierre is cleaner.
David Aspinall
2010-09-09
Hack regexps so that goals are cleared on Proof Completed. message. Unfortun...
David Aspinall
2010-09-09
Fixed the cleaning of goals buffer when proof completed
Pierre Courtieu
2010-09-09
Moved the modeline dislpay of open goals to scripting buffer.
Pierre Courtieu
2010-09-08
Adjust configuration setting for automatic multiple files handling
David Aspinall
2010-09-06
Minor clean up of comments while reading code
David Aspinall
2010-09-01
Fixed experimental feature of storing response or goal in a persistent
Pierre Courtieu
2010-09-01
Fixed bug #346. Coq code was using proof-ids-to-regexp on regexp
Pierre Courtieu
2010-08-30
Response freeze given non special buffer name (Trac #347)
David Aspinall
2010-08-27
Replace proof-terminal-char with proof-terminal-string.
David Aspinall
2010-08-27
Fix for Trac #343
David Aspinall
2010-08-25
coq-find-and-forget: re-enable trivial optimisation (is it really
David Aspinall
2010-08-25
Revert 10.51. proof-script-command-end-regexp: non-letters after
David Aspinall
2010-08-24
coq-set-state-infos: attempt to fix sync problem here
David Aspinall
2010-08-24
proof-script-command-end-regexp: include \' for end of buffer again
David Aspinall
2010-08-24
proof-script-command-end-regexp: allow any non-letter after a period
David Aspinall
2010-08-24
More whitespace changes
David Aspinall
2010-08-24
Cleanups for Elisp formatting conventions.
David Aspinall
2010-08-24
Minor cleanups
David Aspinall
2010-08-22
Change binding for coq-PrintHint as suggested in Trac #341
David Aspinall
2010-08-15
Remove superfluous spaces (re Trac #331).
David Aspinall
2010-08-13
coq-highlight-error: make robust against proof script buffer deactivating
David Aspinall
2010-07-01
proof-last-locked-span: save-excursion -> with-current-buffer to avoid
David Aspinall
2010-05-17
Fixing the behaviour of the responses-freeze window.
Pierre Courtieu
2010-05-17
Allow SearchAbout to deal with complex queries.
Pierre Courtieu
2010-05-17
Added a "remember this" window. Experimental.
Pierre Courtieu
2010-04-12
Fix coq error utf8 underlining with coq-8.3beta.
Pierre Courtieu
2009-12-03
Change of type for proof-script-span-context-menu-extensions
David Aspinall
[next]