aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Expand)AuthorAge
* coq-find-and-forget: Allow undoing prover processed regionsGravatar David Aspinall2010-10-10
* Fixes in strings/comments from Erik Martin-DorelGravatar David Aspinall2010-10-04
* coq-insert-solve-tactic: added (credit:Erik Martin-Dorel, patch from trac #35...Gravatar David Aspinall2010-10-04
* Rename span-add-self-removing-spanGravatar David Aspinall2010-10-01
* coq-highlight-error: use span-add-self-removing-span (highlight and removal i...Gravatar David Aspinall2010-10-01
* coq-allow-highlight-error: remove this setting, now proof-shell-error-or-inte...Gravatar David Aspinall2010-10-01
* Add key binding fixes from Erik Martin-Dorel (see Trac#359).Gravatar David Aspinall2010-10-01
* Fixed redundant undo limit custom variables.Gravatar Pierre Courtieu2010-09-28
* Revert last change, version from Pierre is cleaner.Gravatar David Aspinall2010-09-09
* Hack regexps so that goals are cleared on Proof Completed. message. Unfortun...Gravatar David Aspinall2010-09-09
* Fixed the cleaning of goals buffer when proof completedGravatar Pierre Courtieu2010-09-09
* Moved the modeline dislpay of open goals to scripting buffer.Gravatar Pierre Courtieu2010-09-09
* Adjust configuration setting for automatic multiple files handlingGravatar David Aspinall2010-09-08
* Minor clean up of comments while reading codeGravatar David Aspinall2010-09-06
* Fixed experimental feature of storing response or goal in a persistentGravatar Pierre Courtieu2010-09-01
* Fixed bug #346. Coq code was using proof-ids-to-regexp on regexpGravatar Pierre Courtieu2010-09-01
* Response freeze given non special buffer name (Trac #347)Gravatar David Aspinall2010-08-30
* Replace proof-terminal-char with proof-terminal-string.Gravatar David Aspinall2010-08-27
* Fix for Trac #343Gravatar David Aspinall2010-08-27
* coq-find-and-forget: re-enable trivial optimisation (is it reallyGravatar David Aspinall2010-08-25
* Revert 10.51. proof-script-command-end-regexp: non-letters afterGravatar David Aspinall2010-08-25
* coq-set-state-infos: attempt to fix sync problem hereGravatar David Aspinall2010-08-24
* proof-script-command-end-regexp: include \' for end of buffer againGravatar David Aspinall2010-08-24
* proof-script-command-end-regexp: allow any non-letter after a periodGravatar David Aspinall2010-08-24
* More whitespace changesGravatar David Aspinall2010-08-24
* Cleanups for Elisp formatting conventions.Gravatar David Aspinall2010-08-24
* Minor cleanupsGravatar David Aspinall2010-08-24
* Change binding for coq-PrintHint as suggested in Trac #341Gravatar David Aspinall2010-08-22
* Remove superfluous spaces (re Trac #331).Gravatar David Aspinall2010-08-15
* coq-highlight-error: make robust against proof script buffer deactivatingGravatar David Aspinall2010-08-13
* proof-last-locked-span: save-excursion -> with-current-buffer to avoidGravatar David Aspinall2010-07-01
* Fixing the behaviour of the responses-freeze window.Gravatar Pierre Courtieu2010-05-17
* Allow SearchAbout to deal with complex queries.Gravatar Pierre Courtieu2010-05-17
* Added a "remember this" window. Experimental.Gravatar Pierre Courtieu2010-05-17
* Fix coq error utf8 underlining with coq-8.3beta.Gravatar Pierre Courtieu2010-04-12
* Change of type for proof-script-span-context-menu-extensionsGravatar David Aspinall2009-12-03
* Replace proof-locked-end -> proof-unprocessed-beginGravatar David Aspinall2009-11-30
* Small Fix (again).Gravatar Pierre Courtieu2009-11-20
* Small Fix.Gravatar Pierre Courtieu2009-11-20
* Fix.Gravatar Pierre Courtieu2009-11-11
* fixGravatar Pierre Courtieu2009-11-10
* Fixing insertion case for c-c c-a c-i + cleaning.Gravatar Pierre Courtieu2009-11-10
* Added keyboard shortcut in goals buffer.Gravatar Pierre Courtieu2009-10-15
* Functions find-and-forget and count-undos now return lists of commandsGravatar David Aspinall2009-09-28
* Fixed error highlighting with utf8.Gravatar Pierre Courtieu2009-09-17
* Fix compile warningsGravatar David Aspinall2009-09-16
* Fix highlighting of error regionGravatar David Aspinall2009-09-15
* Surpress warnings for dynamic scopingGravatar David Aspinall2009-09-14
* Remove proof-strict-read-only-toggle call (no longer defined, andGravatar David Aspinall2009-09-14
* Change mode namesGravatar David Aspinall2009-09-14