Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Run make autoloads | 2018-08-23 | |
| | |||
* | Fix most doc issues raised by (checkdoc) | 2018-08-23 | |
| | |||
* | Bump version from 4.4.1~pre to 4.5-git | 2018-08-22 | |
| | | | | This commit ensures the version number is (version-to-list)-compliant. | ||
* | Merge pull request #200 from craff/master | 2018-08-22 | |
|\ | | | | | Update phox support | ||
* | | Add a missing parameter in advice on font-lock-fontify-keywords-region | 2018-03-07 | |
| | | |||
* | | Update copyright messages and improve the header of elisp files. | 2018-02-21 | |
| | | |||
* | | Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228) | 2018-02-20 | |
| | | | | | | Close ProofGeneral/PG#31 | ||
| * | phox is back | 2017-09-22 | |
|/ | |||
* | Fix pg-{show,hide}-all-proofs and Move them into pg-user.el. | 2017-08-15 | |
| | | | | This commit address ProofGeneral/PG#193. | ||
* | Fix easycrypt automode regexp | 2017-06-19 | |
| | | | | | Without the string-end regexp matches all the file names which match the regexp `.eca?`. | ||
* | Fixing bug #187 by removing trailing spaces from prog name. | 2017-06-06 | |
| | |||
* | Remove mmm and ML4PG contribs and remove references to them in code and docs | 2017-05-24 | |
| | |||
* | Change (eval-when (compile) ...) to (eval-when-compile ...) | 2017-05-05 | |
| | | | | This fixes a bunch of compilation warnings | ||
* | Merge pull request #157 from ProofGeneral/elpa | 2017-05-05 | |
|\ | | | | | [WIP] ELPA/MELPA support | ||
* | | Fixing #167. | 2017-03-13 | |
| | | |||
| * | Remove uses of defpgdefault in coq-abbrev | 2017-03-08 | |
| | | | | | | | | | | | | 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'. | ||
| * | Remove compile-time calls to proof-ready-for-assistant | 2017-03-08 | |
| | | | | | | | | | | Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el. | ||
| * | Remove unnecessary calls to 'eval-and-compile' | 2017-03-08 | |
| | | |||
| * | Remove some Emacs <24.1 compatibility cruft | 2017-03-08 | |
| | | |||
| * | Fix incorrect uses of defvar | 2017-03-08 | |
| | | | | | | | | | | | | | | 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. | ||
| * | Fix incorrect assumption that noninteractive == byte-compiling | 2017-03-08 | |
|/ | | | | | The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't. | ||
* | Merge pull request #163 from ProofGeneral/fix_indentation | 2017-03-03 | |
|\ | | | | | Fix indentation | ||
* | | Remove default key-binding for proof-electric-terminator-toggle. | 2017-03-03 | |
| | | | | | | | | Close ProofGeneral/PG#160 | ||
* | | Removing spurious debug messages. | 2017-02-24 | |
| | | |||
* | | Fixing #154. | 2017-02-23 | |
| | | |||
| * | Merge branch 'master' of github.com:ProofGeneral/PG into master_origin | 2017-01-26 | |
| |\ | |/ |/| | |||
| * | annoying missing parentheisis in a comment. | 2017-01-24 | |
| | | |||
* | | save settings not defined with defpacustom (fixes #142) | 2017-01-19 | |
| | | | | | | | | | | | | | | - infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual | ||
* | | split emergency-cleanup to handle interrupts properly (fixes #143) | 2017-01-18 | |
| | | | | | | | | | | | | Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors. | ||
* | | move phox from main to obscure instances | 2017-01-17 | |
| | | | | | | | | | | see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I tried to download phox now, no link was working... | ||
* | | Merge pull request #44 from EasyCrypt/master | 2017-01-17 | |
|\ \ | | | | | | | EasyCrypt PG mode | ||
* | | | Fix prooftree for Coq 8.6 | 2017-01-14 | |
| |/ |/| | | | | | | | | | | | 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. | ||
* | | Merge remote-tracking branch 'OFFICIAL/master' | 2017-01-04 | |
|\ \ | |||
* | | | Fixing #121 + avoid hiding user windows too much. | 2017-01-04 | |
| | | | |||
| * | | fix prooftree crash with long evar lines | 2016-12-28 | |
| | | | |||
| * | | fix generic interrupt procedure to interrupt parallel background compilation | 2016-12-14 | |
| | | | |||
| * | | Merge pull request #129 from hendriktews/keep-going | 2016-12-14 | |
|/| | | | | | | | | Keep going | ||
* | | | Merge pull request #132 from Matafou/master | 2016-12-14 | |
|\ \ \ | | | | | | | | | Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying… | ||
| * | | | remove default absolute name from coq-prog-name, but keep dipsplaying it ↵ | 2016-12-12 | |
| | | | | | | | | | | | | | | | | when asking for it. | ||
| | * | | option coq-compile-keep-going for parallel compilation | 2016-12-08 | |
| |/ / |/| | | | | | | | | | | | | | | With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error. | ||
* | | | fix 2 compilation warnings (fixes #33) | 2016-11-30 | |
|/ / | |||
* | | fix error in process filter: Cannot resize window | 2016-11-02 | |
| | | |||
* | | proof-retract-before-change: Fix #41 by saving/restoring the match data. | 2016-09-25 | |
| | | |||
* | | Bump version number for next release cycle. | 2016-09-19 | |
| | | |||
* | | Update the documentation and prepare the release 4.4. | 2016-09-18 | |
| | | |||
* | | Fix reference to log-warning-minimum-level | 2016-09-16 | |
| | | | | | | Fixes #110. | ||
* | | Ensure PG overlays have pg-span property (#98) | 2016-08-25 | |
| | | |||
* | | Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta). | 2016-07-04 | |
| | | |||
* | | Reset proof-script-buffer to nil if -ready-prover fails | 2016-06-10 | |
| | | | | | | | | Fixes #65 | ||
* | | Update PG's logo | 2016-05-24 | |
| | | | | | | | | | | | | | | 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! |