aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Expand)Author
2021-03-21Fix #562. Lazy/multi_?match indentation support.Pierre Courtieu
2021-03-21Fix #563 avoid dual-send bug in search blacklist customization.Pierre Courtieu
2021-03-17coq: Update coq-prettify-symbols-alist for consistency with company-coqClément Pit-Claudel
2021-02-22protect uses of coq-callcoqHendrik Tews
2021-02-13improve/fix code documentation for vok processingHendrik Tews
2021-02-13add second stage -vok for Coq >= 8.11Hendrik Tews
2021-02-13generalize vio2vo symbol names for vok compilationHendrik Tews
2021-01-31fix typos and unicode single quotations in doc stringsHendrik Tews
2021-01-15Preventive support of "goal instead of "subgoal" in coq messages.Pierre Courtieu
2021-01-10add Coq compile test for a delayed requireHendrik Tews
2020-12-26make-temp-file without text argument for emacs 25Hendrik Tews
2020-12-19ensure vo compilation for tests, increase parallelism, more config outputHendrik Tews
2020-12-19fix 2 background compilation bugs for a dependency in state readyHendrik Tews
2020-12-19add test for recompilation with changesHendrik Tews
2020-12-19fix keep-going when dependency exists but failedHendrik Tews
2020-12-19redesign of parallel background compilation without clonesHendrik Tews
2020-12-07protect coq-callcoq against escaping signalsHendrik Tews
2020-12-07fix coq-callcoq for emacs 27Hendrik Tews
2020-11-19coq: Add highlighting for Hint ModeClément Pit-Claudel
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-10-14Highlight ComputeLi-yao Xia
2020-09-11fix(coq/coq.el): spelling of "whether" (#512)dymil
2020-06-19coq-par-compile: use hash for ancestorsHendrik Tews
2020-06-15Add coloration for Ltac2 commandsCyril Anaclet
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-29WIP for #487Cyril 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-28Merge pull request #496Erik Martin-Dorel
2020-05-28Added a few coq commands.Pierre Courtieu
2020-05-28fix: test files should not provide featuresErik Martin-Dorel
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-15menu entry for coq-compile-vosHendrik Tews
2020-04-15coq-par-compile: support -vos for coq >= 8.11 and default setting changeHendrik Tews
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:03:06 +0000