| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Bump version from 4.4.1~pre to 4.5-git |  Erik Martin-Dorel | 2018-08-22 |
| | | | | | This commit ensures the version number is (version-to-list)-compliant. | ||
| * | Merge pull request #200 from craff/master | Erik Martin-Dorel | 2018-08-22 |
| |\ | | | | | Update phox support | ||
| * | | Add a missing parameter in advice on font-lock-fontify-keywords-region |  Clément Pit--Claudel | 2018-03-07 |
| | | | |||
| * | | Update copyright messages and improve the header of elisp files. | Erik Martin-Dorel | 2018-02-21 |
| | | | |||
| * | | Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228) | Erik Martin-Dorel | 2018-02-20 |
| | | | | | | | Close ProofGeneral/PG#31 | ||
| | * | phox is back |  Christophe Raffalli | 2017-09-22 |
| |/ | |||
| * | Fix pg-{show,hide}-all-proofs and Move them into pg-user.el. | Erik Martin-Dorel | 2017-08-15 |
| | | | | | This commit address ProofGeneral/PG#193. | ||
| * | Fix easycrypt automode regexp |  Mario Rodas | 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. |  Pierre Courtieu | 2017-06-06 |
| | | |||
| * | Remove mmm and ML4PG contribs and remove references to them in code and docs |  Paul Steckler | 2017-05-24 |
| | | |||
| * | Change (eval-when (compile) ...) to (eval-when-compile ...) | Clément Pit--Claudel | 2017-05-05 |
| | | | | | This fixes a bunch of compilation warnings | ||
| * | Merge pull request #157 from ProofGeneral/elpa |  Clément Pit-Claudel | 2017-05-05 |
| |\ | | | | | [WIP] ELPA/MELPA support | ||
| * | | Fixing #167. | Pierre Courtieu | 2017-03-13 |
| | | | |||
| | * | Remove uses of defpgdefault in coq-abbrev | Clément Pit--Claudel | 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 | Clément Pit--Claudel | 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' | Clément Pit--Claudel | 2017-03-08 |
| | | | |||
| | * | Remove some Emacs <24.1 compatibility cruft | Clément Pit--Claudel | 2017-03-08 |
| | | | |||
| | * | Fix incorrect uses of defvar | Clément Pit--Claudel | 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 | Clément Pit--Claudel | 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 |  Pierre Courtieu | 2017-03-03 |
| |\ | | | | | Fix indentation | ||
| * | | Remove default key-binding for proof-electric-terminator-toggle. | Erik Martin-Dorel | 2017-03-03 |
| | | | | | | | | | Close ProofGeneral/PG#160 | ||
| * | | Removing spurious debug messages. | Pierre Courtieu | 2017-02-24 |
| | | | |||
| * | | Fixing #154. | Pierre Courtieu | 2017-02-23 |
| | | | |||
| | * | Merge branch 'master' of github.com:ProofGeneral/PG into master_origin | Pierre Courtieu | 2017-01-26 |
| | |\ | |/ |/| | |||
| | * | annoying missing parentheisis in a comment. | Pierre Courtieu | 2017-01-24 |
| | | | |||
| * | | save settings not defined with defpacustom (fixes #142) |  Hendrik Tews | 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) | Hendrik Tews | 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 | Hendrik Tews | 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 | hendriktews | 2017-01-17 |
| |\ \ | | | | | | | EasyCrypt PG mode | ||
| * | | | Fix prooftree for Coq 8.6 | Hendrik Tews | 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' | Pierre Courtieu | 2017-01-04 |
| |\ \ | |||
| * | | | Fixing #121 + avoid hiding user windows too much. | Pierre Courtieu | 2017-01-04 |
| | | | | |||
| | * | | fix prooftree crash with long evar lines | Hendrik Tews | 2016-12-28 |
| | | | | |||
| | * | | fix generic interrupt procedure to interrupt parallel background compilation | Hendrik Tews | 2016-12-14 |
| | | | | |||
| | * | | Merge pull request #129 from hendriktews/keep-going | hendriktews | 2016-12-14 |
| |/| | | | | | | | | Keep going | ||
| * | | | Merge pull request #132 from Matafou/master | Pierre Courtieu | 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 ↵ | Pierre Courtieu | 2016-12-12 |
| | | | | | | | | | | | | | | | | | when asking for it. | ||
| | | * | | option coq-compile-keep-going for parallel compilation | Hendrik Tews | 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) | Hendrik Tews | 2016-11-30 |
| |/ / | |||
| * | | fix error in process filter: Cannot resize window | Hendrik Tews | 2016-11-02 |
| | | | |||
| * | | proof-retract-before-change: Fix #41 by saving/restoring the match data. | Erik Martin-Dorel | 2016-09-25 |
| | | | |||
| * | | Bump version number for next release cycle. | Erik Martin-Dorel | 2016-09-19 |
| | | | |||
| * | | Update the documentation and prepare the release 4.4. | Erik Martin-Dorel | 2016-09-18 |
| | | | |||
| * | | Fix reference to log-warning-minimum-level | psteckler | 2016-09-16 |
| | | | | | | | Fixes #110. | ||
| * | | Ensure PG overlays have pg-span property (#98) |  Tej Chajed | 2016-08-25 |
| | | | |||
| * | | Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta). |  Erik Martin-Dorel | 2016-07-04 |
| | | | |||
| * | | Reset proof-script-buffer to nil if -ready-prover fails | Clément Pit--Claudel | 2016-06-10 |
| | | | | | | | | | Fixes #65 | ||
| * | | Update PG's logo | Clément Pit--Claudel | 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! | ||
| * | | More version number fixes | Clément Pit--Claudel | 2016-02-13 |
| | | | |||
| | * | Import EasyCrypt PG mode |  Pierre-Yves Strub | 2016-01-29 |
| |/ | |||
 |
index : proof-general | |
| Emacs interface for proof assistants |
| aboutsummaryrefslogtreecommitdiffhomepage |