aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
* Replace proof-terminal-char with proof-terminal-string.Gravatar David Aspinall2010-08-27
|
* Fix for Trac #343Gravatar David Aspinall2010-08-27
|
* Make tests succeed, although still two or three underlying bugsGravatar David Aspinall2010-08-25
|
* coq-find-and-forget: re-enable trivial optimisation (is it reallyGravatar David Aspinall2010-08-25
| | | | slow in Coq to issue a trivial backtrack to the same spot?)
* Revert 10.51. proof-script-command-end-regexp: non-letters afterGravatar David Aspinall2010-08-25
| | | | periods are used in some notations (e.g. SSReflect). See Trac #296.
* 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
| | | | | to terminate a command, fixing #296 (and hopefully not messing up other cases).
* More whitespace changesGravatar David Aspinall2010-08-24
|
* Cleanups for Elisp formatting conventions.Gravatar David Aspinall2010-08-24
| | | | Fix tags handling to work for GNU Emacs etags.el
* Minor cleanupsGravatar David Aspinall2010-08-24
|
* coq-comment-at-point: avoid error if command start not foundGravatar David Aspinall2010-08-24
| | | | (see Trac #342)
* 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
|
* Moved filesGravatar David Aspinall2010-08-15
|
* More testsGravatar David Aspinall2010-08-13
|
* coq-highlight-error: make robust against proof script buffer deactivatingGravatar David Aspinall2010-08-13
|
* Comment out some lines so that processes.Gravatar David Aspinall2010-08-13
|
* Updated.Gravatar David Aspinall2010-08-13
|
* Renamed fileGravatar David Aspinall2010-08-13
|
* Remove deliberately buggy code at the end (Coq seems to be fixed)Gravatar David Aspinall2010-08-11
|
* Try to fix processing of this fileGravatar David Aspinall2010-08-11
|
* UpdateGravatar David Aspinall2010-08-03
|
* proof-last-locked-span: save-excursion -> with-current-buffer to avoidGravatar David Aspinall2010-07-01
| | | | spurious warning in Emacs 23.2
* 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
|
* Point to Trac #313Gravatar David Aspinall2009-12-01
|
* CommentsGravatar David Aspinall2009-12-01
|
* 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
|
* Some more tokensGravatar David Aspinall2009-10-02
|
* Functions find-and-forget and count-undos now return lists of commandsGravatar David Aspinall2009-09-28
|
* Added some more syntax keywords. Made admit tactic with its own redGravatar Pierre Courtieu2009-09-17
| | | | culpabilizing face.
* Added some syntax keywords thanks to Mathieu Sozeau.Gravatar Pierre Courtieu2009-09-17
|
* 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
| | | | | anyway wrong technique). Instead use inhibit-read-only to allow write in possibly read-only area.
* Change mode namesGravatar David Aspinall2009-09-14
|
* Move (require 'local-vars-list) to coq-local-varsGravatar David Aspinall2009-09-10
|
* Move (require 'local-vars-list) from coq.elGravatar David Aspinall2009-09-10
|