aboutsummaryrefslogtreecommitdiff
path: root/coq/coq-abbrev.el
AgeCommit message (Expand)Author
2021-03-21Fix #563 avoid dual-send bug in search blacklist customization.Pierre Courtieu
2021-02-13add second stage -vok for Coq >= 8.11Hendrik Tews
2020-05-29Fix name clash & rephrase some stringsErik Martin-Dorel
2020-05-29First try for feature #487Cyril Anaclet
2020-04-15menu entry for coq-compile-vosHendrik Tews
2020-04-15Span menu entry for proof using annotation + doc.Pierre Courtieu
2020-04-09Merge branch 'master' of https://github.com/ProofGeneral/PGPierre Courtieu
2020-04-09Automatic "Proof using" insertion.Pierre Courtieu
2020-04-01SearchAbout is deprecated since 8.5; use Search insteadClément Pit-Claudel
2019-05-16Highlight diffs in goals and some error messagesJim Fehrle
2019-05-02Fix typosJim Fehrle
2018-12-15Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Stefan Monnier
2018-08-23Fix most doc issues raised by (checkdoc)Erik Martin-Dorel
2018-02-21Update copyright messages and improve the header of elisp files.Erik Martin-Dorel
2017-05-24Remove mmm and ML4PG contribs and remove references to them in code and docsPaul Steckler
2017-05-05Merge pull request #157 from ProofGeneral/elpaClément Pit-Claudel
2017-03-22Added support for future new options (trunk).Pierre Courtieu
2017-03-08Remove uses of defpgdefault in coq-abbrevClément Pit--Claudel
2017-03-08Fix incorrect assumption that noninteractive == byte-compilingClément Pit--Claudel
2017-01-19save settings not defined with defpacustom (fixes #142)Hendrik Tews
2016-12-15Merge pull request #101 from tchajed/print-universes-optionhendriktews
2016-12-14fix generic interrupt procedure to interrupt parallel background compilationHendrik Tews
2016-12-08option coq-compile-keep-going for parallel compilationHendrik Tews
2016-11-18reconcile menu for auto compilationHendrik Tews
2016-11-16first version for quick compilationHendrik Tews
2016-08-15Add Set Printing Universes to options menuTej Chajed
2016-08-14Sort the OPTIONS menu items differently & Fix a typo (UnSet -> Unset).Erik Martin-Dorel
2016-08-14Replace "Set Implicit Arguments" option with "Set Printing Implicit".Erik Martin-Dorel
2015-12-09Adding an setting for Search Blacklist coq option.Pierre Courtieu
2015-10-12proof-assert-command-hook added + Auto adjust width in coq mode.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
2014-12-09Added a variant of searchAbout hiding some spurious entries.Pierre Courtieu
2013-07-22Fixing coq project file parsing + moved project options.Pierre Courtieu
2013-05-30ML4PG functionality added to Coq menujoheras
2012-09-25Fixed #419: coq synchronized variables are not anymore in the settingsPierre Courtieu
2012-09-25Added a menu to set the 3 windows layout.Pierre Courtieu
2012-09-05Fixed double hit terminator. Now it is disabled by default, andPierre Courtieu
2012-08-31Changed the behaviour of proof-layout-windows. Now it follows thePierre Courtieu
2012-07-22Making better menus for Coq. Menus visible in response and goals buffer.Pierre Courtieu
2012-07-09Added completion to insert Require, based on coq-load-path.Pierre Courtieu
2012-07-09Fixed a small bug in indentation + added new commands for queries withPierre Courtieu
2011-06-07Summary: coq-smie: improve indentation.Stefan Monnier
2011-01-18Alternative fix to #382.David Aspinall
2011-01-18Fix trac 382 by not setting save-abbrevs.Pierre Courtieu
2010-09-01Fixed experimental feature of storing response or goal in a persistentPierre Courtieu
2009-09-08CommentsDavid Aspinall
2009-09-06Move holes menu to holes modeDavid Aspinall
2009-09-06Moved doc of holes to holes-modeDavid Aspinall
2009-09-05Clean whitespaceDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:01:28 +0000