aboutsummaryrefslogtreecommitdiff
path: root/generic
AgeCommit message (Expand)Author
2020-06-18Use `proof-shell-string-match-safe` to avoid failing on `nil` regexpPhilipp G. Haselwarter
2020-06-04New hook for early prompt/output analyzis.Pierre Courtieu
2020-05-29fix: backtrack for "Show Proof" disabledAnaclet
2020-05-29fix: backtrack wrong type argumentAnaclet
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-28Fix default value for proof-shell-last-cmd-left-goals-p.Pierre Courtieu
2020-05-27Add proof-shell-last-cmd-left-goals-p.Pierre Courtieu
2020-04-16Fix hide/show proof.Pierre Courtieu
2020-04-15Span menu entry for proof using annotation + doc.Pierre Courtieu
2020-04-10Fixed proof using annotation mechanism.Pierre Courtieu
2020-03-13Fix 464: proof-autoloads not found by EmacsPierre Courtieu
2020-01-31faces: Extend highlights to EOL to adjust for latest Emacs changesClément Pit-Claudel
2019-06-18Remove pghelp spans when retracting.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-31Remove stray hTej Chajed
2019-05-31* coq/coq-diffs.el (coq-insert-tagged-text): Rework to avoid `aset`Stefan Monnier
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-04-18Derive proof-mode from prog-modeBenjamin Barenblat
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
2018-12-22* coq-mode.el: New file to make coq-mode independent from PGStefan Monnier
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-13Use `cl-lib` instead of `cl` everywhereStefan Monnier
2018-12-12Cleanup patch; Moving defvar to toplevelStefan Monnier
2018-11-12Remove code that hides mode-line.Calvin Beck
2018-09-01Reloading proof-autoloads is safe; don't forbid itClément Pit-Claudel
2018-08-25Merge pull request #169 from ProofGeneral/help-span-extendedErik Martin-Dorel
2018-08-23Run make autoloadsErik Martin-Dorel
2018-08-23Fix most doc issues raised by (checkdoc)Erik Martin-Dorel
2018-08-22Bump version from 4.4.1~pre to 4.5-gitErik Martin-Dorel
2018-08-22Merge pull request #200 from craff/masterErik Martin-Dorel
2018-03-07Add a missing parameter in advice on font-lock-fontify-keywords-regionClément Pit--Claudel
2018-02-21Update copyright messages and improve the header of elisp files.Erik Martin-Dorel
2018-02-20Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228)Erik Martin-Dorel
2017-09-22phox is backChristophe Raffalli
2017-08-15Fix pg-{show,hide}-all-proofs and Move them into pg-user.el.Erik Martin-Dorel
2017-06-19Fix easycrypt automode regexpMario Rodas
2017-06-06Fixing bug #187 by removing trailing spaces from prog name.Pierre Courtieu
2017-05-24Remove mmm and ML4PG contribs and remove references to them in code and docsPaul Steckler