aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Expand)Author
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
2020-04-09Merge branch 'master' of https://github.com/ProofGeneral/PGPierre Courtieu
2020-04-09Automatic "Proof using" insertion.Pierre Courtieu
2020-04-02Merge pull request #474 from tchajed/add-ltac2-syntaxErik Martin-Dorel
2020-04-02Add support for core Ltac2 syntaxTej Chajed
2020-04-01SearchAbout is deprecated since 8.5; use Search insteadClément Pit-Claudel
2020-04-01Change "" into nil in argument to appendClément Pit-Claudel
2020-03-26Cleaning previous commit, following @cpitclaudel advices.Pierre Courtieu
2020-03-26Fix #472. Removed -topfile when file name incorrect.Pierre Courtieu
2020-03-12moving tests for monadic notations and Equations in separate files.Pierre Courtieu
2020-03-12Fix #465: Indentation of Equations (plugin).Pierre Courtieu
2020-03-02Adding Tests for indentation related to plugins.Pierre Courtieu
2020-03-02Fix #462.Pierre Courtieu
2020-01-19Generic monadic indentation + specifically ext-lib / Compcert + doc.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:55:29 +0000