aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-config.el
AgeCommit message (Expand)Author
2021-04-16omit proofs: emit warning on nested proofs and continueHendrik Tews
2021-04-16add feature to omit complete opaque proofsHendrik Tews
2021-03-17Remove evaluate-elisp-comment-regexp and set-elisp-variable-regexpClément Pit-Claudel
2021-01-31fix typos and unicode single quotations in doc stringsHendrik Tews
2020-06-04New hook for early prompt/output analyzis.Pierre Courtieu
2020-05-29Apply reviews of @erikmdCyril 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-15Span menu entry for proof using annotation + doc.Pierre Courtieu
2020-04-10Fixed proof using annotation mechanism.Pierre Courtieu
2019-05-16proof-assistant-format: Support format character "%l" a.k.a. lambdaErik Martin-Dorel
2018-08-23Fix most doc issues raised by (checkdoc)Erik Martin-Dorel
2018-02-21Update copyright messages and improve the header of elisp files.Erik Martin-Dorel
2017-02-23Fixing #154.Pierre Courtieu
2016-12-14fix generic interrupt procedure to interrupt parallel background compilationHendrik Tews
2015-10-13proof-retract-command-hook added + more auto adjust width in coq mode.Pierre Courtieu
2015-10-12proof-assert-command-hook added + Auto adjust width in coq mode.Pierre Courtieu
2015-10-09Fixing 4096 character limit of scomint-send-input.Pierre Courtieu
2015-02-04cleaned previous commits (generic variable to disable error coloring).Pierre Courtieu
2014-12-18Fixed response display spurious newlines for coq.Pierre Courtieu
2012-11-13- first version of parallel asynchronous compilation for coq inHendrik Tews
2012-09-14proof-shell-process-connection-type: try using pipes by default in Emacs 24,David Aspinall
2012-01-09Improve configuration for HOL Light. Allow goals display to be prefixed by i...David Aspinall
2012-01-09proof-shell-end-goals-regexp doc: fix inaccuracy, goals always startDavid Aspinall
2012-01-03merge ProofTreeBranch into main trunk:Hendrik Tews
2011-12-06fix a log of broken customization typesHendrik Tews
2011-11-15Quick stab at support for switching to proof shell when interactive support e...David Aspinall
2011-10-13To fix pgshell mode, restore proof-shell-insert support for a single string a...David Aspinall
2011-05-05- flushed proof-done-advancing-require-function andHendrik Tews
2011-04-13proof-shell-insert-hook: Clean docstring, addressing #396.David Aspinall
2011-01-23Make proof-shell-quit-timeout a prover-specific customize option, default to ...David Aspinall
2011-01-23Fix typoDavid Aspinall
2011-01-18- fixed compilation errorsHendrik Tews
2011-01-14- move proof-no-fully-processed-buffer to generic/proof-configHendrik Tews
2011-01-12Add preliminary support for multiple files for coq.Hendrik Tews
2010-12-16Patch to add pgipfloat type.David Aspinall
2010-09-29Support proof-shell-init-cmd being a listDavid Aspinall
2010-08-27Replace proof-terminal-char with proof-terminal-string.David Aspinall
2010-08-24Reduce quit timeout to sensible valueDavid Aspinall
2010-08-19proof-shell-process-connection-type: Revert to long-lived previous default of...David Aspinall
2010-08-18proof-shell-process-connection-type: remove near obsolete test and textDavid Aspinall
2010-08-17Clean up handling of pending interrupts, remove experimental proof-shell-inte...David Aspinall
2010-08-15proof-shell-interrupts-after-commit: support commit-before-interrupt mode [ex...David Aspinall
2010-08-08Checkdoc cleanupsDavid Aspinall
2009-12-04docstringDavid Aspinall
2009-11-30Replace proof-locked-end -> proof-unprocessed-beginDavid Aspinall
2009-11-30even higher proof-shell-quit-timeout -- saving main HOL takes 20s on a *fast*...Makarius Wenzel
2009-11-29raised proof-shell-quit-timeout to accomodate bulky write-back images;Makarius Wenzel