aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2017-03-03Remove default key-binding for proof-electric-terminator-toggle.Erik Martin-Dorel
2016-12-08documentation and CHANGES for coq-compile-keep-goingHendrik Tews
2016-11-30write CHANGESHendrik Tews
2016-10-16Update CHANGES.Erik Martin-Dorel
2016-09-18Detail.Erik Martin-Dorel
2016-09-18Promote CHANGES since 2820cb68 as related to PG 4.4.Erik Martin-Dorel
2016-07-22Adding the option to highlight susual symbols.Pierre Courtieu
2016-06-23Updating CHANGES.Pierre Courtieu
2016-03-21updating CHANGES to the last commit.Pierre Courtieu
2016-01-19Cleaning CHANGES.Pierre Courtieu
2016-01-06updating CHANGESPierre Courtieu
2015-11-30Updated the CHANGES files, mainly git url.Pierre Courtieu
2015-10-12proof-assert-command-hook added + Auto adjust width in coq mode.Pierre Courtieu
2015-06-23Update to CHANGE.Pierre Courtieu
2015-03-26A command to set coq printing width smartly.Pierre Courtieu
2015-03-13Added a command to send Queries to coq, with completion (C-c C-a C-q).Pierre Courtieu
2015-03-09Added bug fixes in CHANGES.Pierre Courtieu
2015-03-05Fixed stuff in CHANGES.Pierre Courtieu
2015-03-05Customization variables for modules, section and proof indentation.Pierre Courtieu
2015-03-04Fixed compilation issue with previous commit + CHANGE updates.Pierre Courtieu
2015-02-03coloring names in resposne and goalsPierre Courtieu
2015-01-27Fixed a bug in script navigation. Updated CHANGEPierre Courtieu
2015-01-14changed default indentation of match's cases.Pierre Courtieu
2015-01-09Removing non-smie indentation + fix CHANGES.Pierre Courtieu
2015-01-05trying to indent pending forall in the expected wayPierre Courtieu
2014-12-23Supporting more bullets (coq 8.5), like ++ or ++++.Pierre Courtieu
2014-06-04* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.Stefan Monnier
2013-07-04Fixing undeclared variables for compilation.Pierre Courtieu
2013-06-21Added an entry to CHANGEs about coq project fields.Pierre Courtieu
2013-01-21- implement proof-script insertionHendrik Tews
2013-01-17document latest changesHendrik Tews
2013-01-15- support bullets and braces in ProoftreeHendrik Tews
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
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 version...Pierre Courtieu
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
2011-11-15Suggest PG 4.1.1 will be released nextDavid Aspinall
2011-10-14Bump doc version numbers to 4.2pre.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 10:02:02 +0000