| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-06 | Merge pull request #191 from AndreasLoow/proof-layout-windows-doc-formatting | Pierre Courtieu | |
| Formatting fix for proof-layout-windows documentation | |||
| 2017-06-30 | Formatting fix for proof-layout-windows documentation | Andreas Lööw | |
| 2017-06-19 | Merge pull request #189 from marsam/master | Clément Pit-Claudel | |
| Fix easycrypt automode regexp | |||
| 2017-06-19 | Fix easycrypt automode regexp | Mario Rodas | |
| Without the string-end regexp matches all the file names which match the regexp `.eca?`. | |||
| 2017-06-08 | Fixing a bug with Set/Unset commands due to recent commits. | Pierre Courtieu | |
| The "Show" inserted now and then would hide the result of Set/Unset commands. | |||
| 2017-06-06 | Adding a Set Silent + Show when backtracking into a proof. | Pierre Courtieu | |
| Checking whether the backtrack is inside a proof or not is a bit convoluted but seems ok. | |||
| 2017-06-06 | Fixing bug #187 by removing trailing spaces from prog name. | Pierre Courtieu | |
| 2017-05-25 | Merge pull request #185 from psteckler/remove-contribs | psteckler | |
| Remove mmm and ML4PG contribs | |||
| 2017-05-24 | Remove mmm and ML4PG contribs and remove references to them in code and docs | Paul Steckler | |
| 2017-05-23 | Fixing #183. | Pierre Courtieu | |
| 2017-05-16 | Fixing Set/Unset Printing broken by auto "Show". | Pierre Courtieu | |
| Current coq trunk has a bug with Show that I reported (there is a spurious Show executed) which makes C-u C-c C-a C-s fail for now. Should be fixed shortly. | |||
| 2017-05-12 | temporary fix of automatic intros. | Pierre Courtieu | |
| 2017-05-05 | Change (eval-when (compile) ...) to (eval-when-compile ...) | Clément Pit--Claudel | |
| This fixes a bunch of compilation warnings | |||
| 2017-05-05 | Merge pull request #157 from ProofGeneral/elpa | Clément Pit-Claudel | |
| [WIP] ELPA/MELPA support | |||
| 2017-04-25 | Typo from commit 758e679e. | Pierre Courtieu | |
| 2017-04-25 | [Travis CI] Replace emacs-git target with emacs-25.{1,2} stable targets. (#181) | Erik Martin-Dorel | |
| This commit contributes to shorten the real time of Travis' automated build. | |||
| 2017-04-25 | Remove bin/proofgeneral and Update Makefiles accordingly. | Erik Martin-Dorel | |
| Closes ProofGeneral/PG#177 | |||
| 2017-04-24 | Preparing new warning tags (no more special chars). | Pierre Courtieu | |
| 2017-04-19 | Fix #176. | Pierre Courtieu | |
| The code uses several token searcher and the wrong one was called somewhere. | |||
| 2017-04-18 | Add file contrib/mmm/.nosearch to help feature extraction tools | Jonas Bernoulli | |
| This change is intended as an intermediate step toward the removal of the bundled copy of `mmm' package. Even with this change, PG continues to use the bundled version, unless `mmm-auto' is already loaded at the time PG first loads `proof-auxmodes'. The benefit of this change is that tools that extract the features provided and required by a package, such as those used to maintain the Emacsmirror, will no longer be tricked into believing that `mmm' is part of PG. Eventually the bundled `mmm' copy should be removed completely, as I suggested in #171, and as was already on the roadmap before I did so. | |||
| 2017-04-12 | [doc]: add documentation for the EasyCrypt mode | Pierre-Yves Strub | |
| 2017-03-31 | Fixing #173. | Pierre Courtieu | |
| 2017-03-22 | Added support for future new options (trunk). | Pierre Courtieu | |
| 2017-03-13 | Fixing #167. | Pierre Courtieu | |
| 2017-03-08 | elpa: Add a package file and a package.el-friendly init script | Clément Pit--Claudel | |
| 2017-03-08 | Add a FIXME in coq.el | Clément Pit--Claudel | |
| 2017-03-08 | Remove uses of defpgdefault in coq-abbrev | Clé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-08 | Remove uses of defpacustom in coq-compile-common | Clément Pit--Claudel | |
| This file is `require'-d from other places, at compile time. This doesn't work nicely with compilation by package.el (PG complains and says "defpacustom: Proof assistant setting compile-before-require re-defined!") | |||
| 2017-03-08 | easycrypt: Don't require pg-custom: it breaks compilation | Clément Pit--Claudel | |
| The problem is that loading pg-custom runs a bunch of defpgcustom, with no current proof assistant. Then when coq or easycrypt calls proof-ready-for-assistant, pg-custom isn't loaded again. | |||
| 2017-03-08 | Remove compile-time calls to proof-ready-for-assistant | Clé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-08 | Remove unnecessary calls to 'eval-and-compile' | Clément Pit--Claudel | |
| 2017-03-08 | Remove a few useless eval-and-compile calls | 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 | |
| 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-08 | Fix incorrect assumption that noninteractive == byte-compiling | Clément Pit--Claudel | |
| The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't. | |||
| 2017-03-08 | Merge commit '06fd76163b857a056ac44e7437efa17656f06e5b' | Paul Steckler | |
| 2017-03-08 | Fixing unicode tokens in generic code and in coq. | Pierre Courtieu | |
| 2017-03-06 | get threeb frames only when needed | Paul Steckler | |
| 2017-03-06 | one more redundant call removed | Paul Steckler | |
| 2017-03-06 | remove redundant calls, simplify code | Paul Steckler | |
| 2017-03-03 | Merge pull request #163 from ProofGeneral/fix_indentation | Pierre Courtieu | |
| Fix indentation | |||
| 2017-03-03 | Refreshing goal when Set Printing xxx. (#162) | Pierre Courtieu | |
| * Close ProofGeneral/PG#161. Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open). | |||
| 2017-03-03 | Remove default key-binding for proof-electric-terminator-toggle. | Erik Martin-Dorel | |
| Close ProofGeneral/PG#160 | |||
| 2017-03-02 | use Utf8 from Coq library | Paul Steckler | |
| 2017-02-27 | serveral coqtags fixes and improvements | Hendrik Tews | |
| - precise tags for definitions - fix bug with nonempty white space lines - add several keywords (Proposition, Record, ...) - generate tags for constructors of inductive definitions and for record labels | |||
| 2017-02-27 | Merge pull request #156 from Matafou/fix-154 | Pierre Courtieu | |
| Fixing #154. | |||
| 2017-02-25 | Add easycrypt and twelf to Makefile | Clément Pit--Claudel | |
| 2017-02-24 | Removing spurious debug messages. | Pierre Courtieu | |
| 2017-02-23 | Fixing #154. | Pierre Courtieu | |
| 2017-02-21 | [ec mode]: update keywords | Pierre-Yves Strub | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |