aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-05-31Merge pull request #425 from tchajed/fix-stray-hClément Pit-Claudel
2019-05-31Remove stray hTej Chajed
2019-05-31* coq/coq-diffs.el (coq-insert-tagged-text): Rework to avoid `aset`Stefan Monnier
2019-05-23Merge pull request #421 from jfehrle/for_master2Pierre Courtieu
2019-05-22Merge pull request #423 from Matafou/fix-422Pierre Courtieu
2019-05-22FIX #422.Pierre Courtieu
2019-05-16Do a "Set Diffs" whenever backtracking. This also re-prints theJim Fehrle
2019-05-16proof-syntax.el: Fix an out-of-range bug in function `proof-format'Erik Martin-Dorel
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
2019-04-19Merge pull request #418 from SkySkimmer/clean-argsErik Martin-Dorel
2019-04-19Clean -topfile for coq-prog-args properlyGaëtan Gilbert
2019-04-18Merge pull request #419 from bbarenblat/masterClément Pit-Claudel
2019-04-18Derive proof-mode from prog-modeBenjamin Barenblat
2019-02-12Simpler fix for #411.Pierre Courtieu
2019-02-12Fixes #411.Pierre Courtieu
2019-01-14Hopefully fix ProofGeneral/PG#413Erik Martin-Dorel
2019-01-13Fix ProofGeneral/PG#413 furtherErik Martin-Dorel
2019-01-13Merge pull request #414 from ProofGeneral/improve-use-package-supportErik Martin-Dorel
2019-01-13Update the commentary section in proof-general.elErik Martin-Dorel
2019-01-13Fix the license notice in proof-general.elErik Martin-Dorel
2019-01-13Rename pg-init.el to proof-general.elErik Martin-Dorel
2019-01-12* pg-init.el: Add subdirs during compilation (bug #413)Stefan Monnier
2018-12-26Make coq-mode work without generic/proof-*Stefan Monnier
2018-12-25Reduce the impact of proof-site, in case PG is not usedStefan Monnier
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 08:43:51 +0000