aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Collapse)Author
2013-01-21- implement proof-script insertionHendrik Tews
2013-01-17document latest changesHendrik Tews
2013-01-15- support bullets and braces in ProoftreeHendrik Tews
- prooftree protocol change to version 3
2012-11-15write CHANGESHendrik Tews
2012-10-19Updates for PG 4.3David Aspinall
2012-09-25Fixed a bug in three windows mode.Pierre Courtieu
2012-09-07Added one point + details to CHANGES.Pierre Courtieu
2012-09-05Fixed double hit terminator. Now it is disabled by default, andPierre Courtieu
enabling it disables electric-terminator and vice-versa. In case both are non nil at the same time, then electric teminator has priority. If people like it we may propose this to other modes than coq. + fixed window layout policy.
2012-08-14Add user option proof-next-command-insert-space.David Aspinall
2012-07-24Fixing compilation. Still need to verify some smie stuff on different ↵Pierre Courtieu
versions of emacs.
2012-07-09Added completion to insert Require, based on coq-load-path.Pierre Courtieu
2012-07-09updated CHANGES for Coq.Pierre Courtieu
2012-07-06More fixes in coq indentation.Pierre Courtieu
2012-01-18Added some detail on the indentation limitation in the CHANGE.Pierre Courtieu
2012-01-12Fix typo, mention HOL LightDavid Aspinall
2012-01-04Add link to Prooftree downloadDavid Aspinall
2012-01-03update CHANGESHendrik Tews
2011-12-23Will release 4.2 next, after allDavid Aspinall
2011-12-07- protect proof-shell-handle-delayed-output against the case whereHendrik Tews
proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals
2011-11-15Suggest PG 4.1.1 will be released nextDavid Aspinall
2011-10-14Bump doc version numbers to 4.2pre.David Aspinall
2011-06-22coq-use-smie not enabled by defaultDavid Aspinall
2011-05-16Ref to Coq chapter in PG manualDavid Aspinall
2011-01-25Note recent changesDavid Aspinall
2010-11-15Summary: New indentation code using SMIEStefan Monnier
* coq/coq.el (coq-build-prog-args): Avoid meaningless \- escape sequence. (coq-use-smie): New custom var. (coq-smie-grammar): New var. (coq-smie-rules): New function. (coq-guess-or-ask-for-string): Use use-region-p. (coq-mode-config): Use smie-setup if available. * lib/proof-compat.el (use-region-p): Provide fallback definition.
2010-11-03Updated.David Aspinall
2010-10-13Update for config changes.David Aspinall
2010-10-11proof-use-parser-cache=t defaultDavid Aspinall
2010-10-10Clarify Emacs 22 versionDavid Aspinall
2010-10-10Support Emacs 23.1+ only.David Aspinall
2010-10-01Document query identifierDavid Aspinall
2010-10-01proof-script-command-separator: removed (always a space)David Aspinall
2010-09-21Add Document Centred command. Adjust for new menu layout.David Aspinall
2010-09-09Fixed the cleaning of goals buffer when proof completedPierre Courtieu
+ fixed the refreshing of modeline goal number display.
2010-09-09filled CHANGES a bit more precisely.Pierre Courtieu
2010-09-09Fixed small bugs in indentation.Pierre Courtieu
2010-09-01Fixed bug #346. Coq code was using proof-ids-to-regexp on regexpPierre Courtieu
instead of pure strings.
2010-08-27UpdatedDavid Aspinall
2010-08-20Mention Fast Process BufferDavid Aspinall
2010-08-15Update.David Aspinall
2010-08-03pg-protected-undo changeDavid Aspinall
2010-08-03Updated.David Aspinall
2009-12-04UpdatedDavid Aspinall
2009-10-15UpdatedDavid Aspinall
2009-10-02Explain Unicode Tokens betterDavid Aspinall
2009-09-14UpdatedDavid Aspinall
2009-09-11Elaborate on new settingsDavid Aspinall
2009-09-09*** empty log message ***David Aspinall
2009-09-09*** empty log message ***David Aspinall
2009-09-08Updated.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:14:21 +0000