aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Expand)Author
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
2020-01-13Fixing /\ and \/ priority for indentation purpose.Pierre Courtieu
2019-12-08fix: Recognize "Timeout" before save keywordsErik Martin-Dorel
2019-12-04Uncommented coq-find-comment-start, coq-find-comment-end as quick fix for #444Vadim Zaliva
2019-10-07Make -topfile facility work for unnamed filesKazuhiko Sakaguchi
2019-08-21coq-par-compile: fix 8.10 -schedule-vio2vo incompatibilityHendrik Tews
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-25fix coqtags that can't find some theorem and output empty definition nameYu-Fu Fu
2019-06-17fixing with inductive indentation.Pierre 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-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-22FIX #422.Pierre Courtieu
2019-05-16Do a "Set Diffs" whenever backtracking. This also re-prints theJim Fehrle
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-19Clean -topfile for coq-prog-args properlyGaëtan Gilbert
2019-02-12Simpler fix for #411.Pierre Courtieu
2019-02-12Fixes #411.Pierre Courtieu
2018-12-26Make coq-mode work without generic/proof-*Stefan Monnier
2018-12-22* coq-mode.el: New file to make coq-mode independent from PGStefan Monnier
2018-12-20Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2018-12-20Fixes #395: hyps highlight is transient and with gray background.Pierre Courtieu
2018-12-19Quote ?( ?)soraros
2018-12-15Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Stefan Monnier
2018-12-15Prepend cl- to more c[ad]+r instancesClément Pit-Claudel
2018-12-15Use cl-caddr instead of caddrClément Pit-Claudel
2018-12-14Fix remaining uses of CL; Make files more declarativeStefan Monnier
2018-12-14Fixes the fix of #407. Is this temporary.Pierre Courtieu
2018-12-14Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2018-12-14Fix #407: -topfile added if coq > v8.10alpha.Pierre Courtieu
2018-12-13Use `cl-lib` instead of `cl` everywhereStefan Monnier
2018-12-12Cleanup patch; Moving defvar to toplevelStefan Monnier
2018-11-01Ignore ephemeral buffers, and buffers not pointed at files.Calvin Beck
2018-10-30Use non-remote path to expand paths in _CoqProject when file is remote.Daniel Patterson
2018-09-27Fix parsing of -arg in _CoqProject fileAnton Trunov
2018-08-23Fix most doc issues raised by (checkdoc)Erik Martin-Dorel
2018-08-21Merge pull request #379 from tchajed/variant-keywordClément Pit-Claudel
2018-08-18Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2018-08-18Fix #7980, keep option order unchanged.Pierre Courtieu
2018-08-17Support the Variant vernacularTej Chajed
2018-08-07Add coq-Print-Ltac to print an Ltac termJohn Grosen
2018-06-15Fixing last commit.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:16:27 +0000