aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-04-29fix: coq-tests.el and related filesErik Martin-Dorel
2020-04-29fix(test.sh): $_dir namingErik Martin-Dorel
2020-04-29Add ERT tests (WIP)Cyril Anaclet
2020-04-29Add a testCyril Anaclet
2020-04-27[CI] fail-fast:=falseErik Martin-Dorel
2020-04-27[CI] Use coq-community/docker-coq-action@v1Erik Martin-Dorel
2020-04-22[CI] Use erikmd/docker-coq-action@masterErik Martin-Dorel
2020-04-21Merge pull request #483 from ProofGeneral/use-github-actionsErik Martin-Dorel
2020-04-21docs(README.md): Update CI badgeErik Martin-Dorel
2020-04-21[CI] Tweak max-parallel specErik Martin-Dorel
2020-04-21[CI] Fix on/(push,pull_request) specErik Martin-Dorel
2020-04-21s/4.07-flambda/minimal/Erik Martin-Dorel
2020-04-21fix: Install emacs in the Docker containerErik Martin-Dorel
2020-04-17feat: Update test.yml to trigger integration testsErik Martin-Dorel
2020-04-17feat: Add first version of coq-tests.elErik Martin-Dorel
2020-04-17chore: Add shell script to automate the testsErik Martin-Dorel
2020-04-16chore: Add init-tests.elErik Martin-Dorel
2020-04-16feat: Add GitHub-action workflowErik Martin-Dorel
2020-04-16feat: Remove Travis CI configurationErik Martin-Dorel
2020-04-16Fix hide/show 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-15add CHANGES entry for vosHendrik Tews
2020-04-15update documentation for vos compilationHendrik Tews
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-10docs: Update CHANGES after issue #479 and PR #480Erik Martin-Dorel
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-02Rephrase ProofGeneral.texi following PR #476 that fixed #475Erik Martin-Dorel
2020-04-02Merge pull request #476 from dunnl/issue-475Erik Martin-Dorel
2020-04-02Correct documentationLawrence Dunn
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-13Fix 464: proof-autoloads not found by EmacsPierre 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-02-06Merge pull request #455 from ProofGeneral/cpitclaudel_extend_facesClément Pit-Claudel