aboutsummaryrefslogtreecommitdiff
path: root/coq/coq.el
AgeCommit message (Expand)Author
2021-04-21Merge pull request #559 from hendriktews/omit-proofsHEADmasterErik Martin-Dorel
2021-04-16add feature to omit complete opaque proofsHendrik Tews
2021-04-08Fixing "match with" generation.Pierre Courtieu
2021-04-08Fixing hypothesis folding GUI.Pierre Courtieu
2021-03-21Fix #563 avoid dual-send bug in search blacklist customization.Pierre Courtieu
2021-01-15Preventive support of "goal instead of "subgoal" in coq messages.Pierre Courtieu
2020-10-16Fix #514 + support for named goal selector.Pierre Courtieu
2020-10-16Fix #518: "Proof using" mode corrupts "Proof with tac".Pierre Courtieu
2020-09-11fix(coq/coq.el): spelling of "whether" (#512)dymil
2020-06-04New hook for early prompt/output analyzis.Pierre Courtieu
2020-05-29Minor changesAnaclet
2020-05-29fix: backtrack for "Show Proof" disabledAnaclet
2020-05-29fix: backtrack wrong type argumentAnaclet
2020-05-29fix: Do "Show Proof…" (with "?Goal") as soon as the proof is startedErik Martin-Dorel
2020-05-29Apply reviews of @erikmdCyril Anaclet
2020-05-29Fix name clash & rephrase some stringsErik Martin-Dorel
2020-05-29All case for Show and regex variableCyril Anaclet
2020-05-29First try for feature #487Cyril Anaclet
2020-05-27Add proof-shell-last-cmd-left-goals-p.Pierre Courtieu
2020-05-04Fixing #485, bug on proof without "Proof".Pierre Courtieu
2020-04-15Fix a bug in detection of "Proof." when "proof using" insertionPierre Courtieu
2020-04-15Fixed disabled proof using menu.Pierre Courtieu
2020-04-15Span menu entry for proof using annotation + doc.Pierre Courtieu
2020-04-10Merge branch 'master' of https://github.com/ProofGeneral/PGPierre Courtieu
2020-04-10Fixed proof using annotation mechanism.Pierre Courtieu
2020-04-10Merge pull request #480 from CyrilAnac/masterErik Martin-Dorel
2020-04-10Close #479cyrilzak31
2020-04-09Unplugging previous commit (proof using insertion.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-07-26fix: Add missing "Set Diffs ..." command in some backtracking caseErik Martin-Dorel
2019-07-26fix: corner case where "Show." was not triggered.Erik Martin-Dorel
2019-07-26Backtrack -> BackToEnrico Tassi
2019-06-03Process tags in the buffer rather than in stringsJim Fehrle
2019-06-01Add hook for coq diff-highlighting routineJim Fehrle
2019-05-16Do a "Set Diffs" whenever backtracking. This also re-prints theJim Fehrle
2019-05-16proof-assistant-format: Support format character "%l" a.k.a. lambdaErik Martin-Dorel
2019-05-16Highlight diffs in goals and some error messagesJim Fehrle
2019-05-02Fix typosJim Fehrle
2018-12-26Make coq-mode work without generic/proof-*Stefan Monnier
2018-12-22* coq-mode.el: New file to make coq-mode independent from PGStefan Monnier
2018-12-20Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2018-12-20Fixes #395: hyps highlight is transient and with gray background.Pierre Courtieu
2018-12-19Quote ?( ?)soraros
2018-12-15Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Stefan Monnier
2018-12-15Prepend cl- to more c[ad]+r instancesClément Pit-Claudel
2018-12-15Use cl-caddr instead of caddrClément Pit-Claudel
2018-12-13Use `cl-lib` instead of `cl` everywhereStefan Monnier
2018-12-12Cleanup patch; Moving defvar to toplevelStefan Monnier
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:23 +0000