aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2021-04-21Document the "Proof using" requirement for 'proof-omit-proofs-optionErik Martin-Dorel
2021-04-16document the omit proofs feature manual and changes fileHendrik Tews
2021-03-21Fix #563 avoid dual-send bug in search blacklist customization.Pierre Courtieu
2021-02-25docs(CHANGES): Add "M-x proof-upgrade-elpa-packages RET" & menu itemErik Martin-Dorel
2021-02-13update changes and documentation for vok featureHendrik Tews
2020-09-11fix(CHANGES): spelling of "whether" (#511)dymil
2020-04-15add CHANGES entry for vosHendrik Tews
2020-04-15Span menu entry for proof using annotation + doc.Pierre Courtieu
2020-04-10docs: Update CHANGES after issue #479 and PR #480Erik Martin-Dorel
2020-04-09Automatic "Proof using" insertion.Pierre Courtieu
2020-01-19Generic monadic indentation + specifically ext-lib / Compcert + doc.Pierre Courtieu
2019-05-16Highlight diffs in goals and some error messagesJim Fehrle
2018-08-22Bump version from 4.4.1~pre to 4.5-gitErik Martin-Dorel
2018-06-11key maps + small glitch hyp highlight/folding code.Pierre Courtieu
2018-06-08Changed the look of folding/unfolding hyps.Pierre Courtieu
2018-06-04Shorter CHANGES + smal fixes in hide/highlight hyps code.Pierre Courtieu
2018-06-01Click hypothesis to (un)hide them.Pierre Courtieu
2018-05-31Updated CHANGES about hiding and highlighting of hyps.Pierre Courtieu
2018-02-20Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228)Erik Martin-Dorel
2017-11-06Prettier cheat face (background + box).Pierre Courtieu
2017-10-26Updating CHANGES with lexer extensibility.Pierre Courtieu
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 06:48:04 +0000