aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-01-31faces: Extend highlights to EOL to adjust for latest Emacs changesClément Pit-Claudel
2020-01-20Merge pull request #452 from Matafou/fix_monadicPierre Courtieu
2020-01-19Generic monadic indentation + specifically ext-lib / Compcert + doc.Pierre Courtieu
2020-01-13Fixing /\ and \/ priority for indentation purpose.Pierre Courtieu
2019-12-09Merge pull request #447 from ProofGeneral/fix-gh-446Erik Martin-Dorel
2019-12-08fix: Recognize "Timeout" before save keywordsErik Martin-Dorel
2019-12-05Merge pull request #445 from vzaliva/patch-1Erik Martin-Dorel
2019-12-04Uncommented coq-find-comment-start, coq-find-comment-end as quick fix for #444Vadim Zaliva
2019-10-07Merge pull request #443 from pi8027/topfile-unnamedErik Martin-Dorel
2019-10-07Make -topfile facility work for unnamed filesKazuhiko Sakaguchi
2019-08-21Merge pull request #438 from hendriktews/fix-vio2vo-8-10Erik Martin-Dorel
2019-08-21coq-par-compile: fix 8.10 -schedule-vio2vo incompatibilityHendrik Tews
2019-07-27Merge pull request #434 from gares/patch-1Clé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-07-25Merge pull request #432 from a0919610611/fix-coqtagsPierre Courtieu
2019-07-25fix coqtags that can't find some theorem and output empty definition nameYu-Fu Fu
2019-06-18Remove pghelp spans when retracting.Pierre Courtieu
2019-06-17fixing with inductive indentation.Pierre Courtieu
2019-06-06Merge pull request #426 from jfehrle/tweakPierre Courtieu
2019-06-03Process tags in the buffer rather than in stringsJim Fehrle
2019-06-01Add hook for coq diff-highlighting routineJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:43:35 +0000