aboutsummaryrefslogtreecommitdiff
path: root/generic
AgeCommit message (Collapse)Author
2018-08-22Bump version from 4.4.1~pre to 4.5-gitErik Martin-Dorel
This commit ensures the version number is (version-to-list)-compliant.
2018-08-22Merge pull request #200 from craff/masterErik Martin-Dorel
Update phox support
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
Close ProofGeneral/PG#31
2017-09-22phox is backChristophe Raffalli
2017-08-15Fix pg-{show,hide}-all-proofs and Move them into pg-user.el.Erik Martin-Dorel
This commit address ProofGeneral/PG#193.
2017-06-19Fix easycrypt automode regexpMario Rodas
Without the string-end regexp matches all the file names which match the regexp `.eca?`.
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
2017-05-05Change (eval-when (compile) ...) to (eval-when-compile ...)Clément Pit--Claudel
This fixes a bunch of compilation warnings
2017-05-05Merge pull request #157 from ProofGeneral/elpaClément Pit-Claudel
[WIP] ELPA/MELPA support
2017-03-13Fixing #167.Pierre Courtieu
2017-03-09extend helpspan, issue #158Paul Steckler
2017-03-08Remove uses of defpgdefault in coq-abbrevClément Pit--Claudel
This file is `require'-d when compiling coq.el, and at that point the proof assistant isn't set to coq yet, so it would define variables prefixed by `nil-' instead of `coq'.
2017-03-08Remove compile-time calls to proof-ready-for-assistantClément Pit--Claudel
Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el.
2017-03-08Remove unnecessary calls to 'eval-and-compile'Clément Pit--Claudel
2017-03-08Remove some Emacs <24.1 compatibility cruftClément Pit--Claudel
2017-03-08Fix incorrect uses of defvarClément Pit--Claudel
It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance.
2017-03-08Fix incorrect assumption that noninteractive == byte-compilingClément Pit--Claudel
The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't.
2017-03-03Merge pull request #163 from ProofGeneral/fix_indentationPierre Courtieu
Fix indentation
2017-03-03Remove default key-binding for proof-electric-terminator-toggle.Erik Martin-Dorel
Close ProofGeneral/PG#160
2017-02-24Removing spurious debug messages.Pierre Courtieu
2017-02-23Fixing #154.Pierre Courtieu
2017-01-26Merge branch 'master' of github.com:ProofGeneral/PG into master_originPierre Courtieu
2017-01-24annoying missing parentheisis in a comment.Pierre Courtieu
2017-01-19save settings not defined with defpacustom (fixes #142)Hendrik Tews
- infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual
2017-01-18split emergency-cleanup to handle interrupts properly (fixes #143)Hendrik Tews
Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors.
2017-01-17move phox from main to obscure instancesHendrik Tews
see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I tried to download phox now, no link was working...
2017-01-17Merge pull request #44 from EasyCrypt/masterhendriktews
EasyCrypt PG mode
2017-01-14Fix prooftree for Coq 8.6Hendrik Tews
In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook.
2017-01-04Merge remote-tracking branch 'OFFICIAL/master'Pierre Courtieu
2017-01-04Fixing #121 + avoid hiding user windows too much.Pierre Courtieu
2016-12-28fix prooftree crash with long evar linesHendrik Tews
2016-12-14fix generic interrupt procedure to interrupt parallel background compilationHendrik Tews
2016-12-14Merge pull request #129 from hendriktews/keep-goinghendriktews
Keep going
2016-12-14Merge pull request #132 from Matafou/masterPierre Courtieu
Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
2016-12-12remove default absolute name from coq-prog-name, but keep dipsplaying it ↵Pierre Courtieu
when asking for it.
2016-12-08option coq-compile-keep-going for parallel compilationHendrik Tews
With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error.
2016-11-30fix 2 compilation warnings (fixes #33)Hendrik Tews
2016-11-02fix error in process filter: Cannot resize windowHendrik Tews
2016-09-25proof-retract-before-change: Fix #41 by saving/restoring the match data.Erik Martin-Dorel
2016-09-19Bump version number for next release cycle.Erik Martin-Dorel
2016-09-18Update the documentation and prepare the release 4.4.Erik Martin-Dorel
2016-09-16Fix reference to log-warning-minimum-levelpsteckler
Fixes #110.
2016-08-25Ensure PG overlays have pg-span property (#98)Tej Chajed
2016-07-04Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta).Erik Martin-Dorel
2016-06-10Reset proof-script-buffer to nil if -ready-prover failsClément Pit--Claudel
Fixes #65
2016-05-24Update PG's logoClément Pit--Claudel
The new art is a contribution of Yoshihiro Imai (http://proofcafe.org/~yoshihiro503/), first released at https://github.com/yoshihiro503/generaltan and kindly made available under the terms of the GPL. Many thanks!
2016-02-13More version number fixesClément Pit--Claudel