aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | Prettier cheat face (background + box).Gravatar Pierre Courtieu2017-11-06
| | | |
* | | | Fix #135.Gravatar Pierre Courtieu2017-11-06
| | | |
* | | | Updating CHANGES with lexer extensibility.Gravatar Pierre Courtieu2017-10-26
| | | |
* | | | Limited extensibility of smie token detection.Gravatar Pierre Courtieu2017-10-26
|/ / /
| * | phox syntax table + more symbolsGravatar Christophe Raffalli2017-09-22
| | |
| * | phox is backGravatar Christophe Raffalli2017-09-22
|/ /
* | Fix pg-{show,hide}-all-proofs and Move them into pg-user.el.Gravatar Erik Martin-Dorel2017-08-15
| | | | | | | | This commit address ProofGeneral/PG#193.
* | changed -emacs-U flag to -emacsGravatar Paul Steckler2017-07-19
| |
* | Merge pull request #191 from AndreasLoow/proof-layout-windows-doc-formattingGravatar Pierre Courtieu2017-07-06
|\ \ | | | | | | Formatting fix for proof-layout-windows documentation
| * | Formatting fix for proof-layout-windows documentationGravatar Andreas Lööw2017-06-30
|/ /
* | Merge pull request #189 from marsam/masterGravatar Clément Pit-Claudel2017-06-19
|\ \ | | | | | | Fix easycrypt automode regexp
| * | Fix easycrypt automode regexpGravatar Mario Rodas2017-06-19
|/ / | | | | | | | | Without the string-end regexp matches all the file names which match the regexp `.eca?`.
* | Fixing a bug with Set/Unset commands due to recent commits.Gravatar Pierre Courtieu2017-06-08
| | | | | | | | | | The "Show" inserted now and then would hide the result of Set/Unset commands.
* | Adding a Set Silent + Show when backtracking into a proof.Gravatar Pierre Courtieu2017-06-06
| | | | | | | | | | Checking whether the backtrack is inside a proof or not is a bit convoluted but seems ok.
* | Fixing bug #187 by removing trailing spaces from prog name.Gravatar Pierre Courtieu2017-06-06
| |
* | Merge pull request #185 from psteckler/remove-contribsGravatar psteckler2017-05-25
|\ \ | | | | | | Remove mmm and ML4PG contribs
| * | Remove mmm and ML4PG contribs and remove references to them in code and docsGravatar Paul Steckler2017-05-24
| | |
* | | Fixing #183.Gravatar Pierre Courtieu2017-05-23
|/ /
* | Fixing Set/Unset Printing broken by auto "Show".Gravatar Pierre Courtieu2017-05-16
| | | | | | | | | | | | 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.
* | temporary fix of automatic intros.Gravatar Pierre Courtieu2017-05-12
| |
* | Change (eval-when (compile) ...) to (eval-when-compile ...)Gravatar Clément Pit--Claudel2017-05-05
| | | | | | | | This fixes a bunch of compilation warnings
* | Merge pull request #157 from ProofGeneral/elpaGravatar Clément Pit-Claudel2017-05-05
|\ \ | | | | | | [WIP] ELPA/MELPA support
* | | Typo from commit 758e679e.Gravatar Pierre Courtieu2017-04-25
| | |
* | | [Travis CI] Replace emacs-git target with emacs-25.{1,2} stable targets. (#181)Gravatar Erik Martin-Dorel2017-04-25
| | | | | | | | | This commit contributes to shorten the real time of Travis' automated build.
* | | Remove bin/proofgeneral and Update Makefiles accordingly.Gravatar Erik Martin-Dorel2017-04-25
| | | | | | | | | | | | Closes ProofGeneral/PG#177
* | | Preparing new warning tags (no more special chars).Gravatar Pierre Courtieu2017-04-24
| | |
* | | Fix #176.Gravatar Pierre Courtieu2017-04-19
| | | | | | | | | | | | | | | The code uses several token searcher and the wrong one was called somewhere.
* | | Add file contrib/mmm/.nosearch to help feature extraction toolsGravatar Jonas Bernoulli2017-04-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | [doc]: add documentation for the EasyCrypt modeGravatar Pierre-Yves Strub2017-04-12
| | |
* | | Fixing #173.Gravatar Pierre Courtieu2017-03-31
| | |
* | | Added support for future new options (trunk).Gravatar Pierre Courtieu2017-03-22
| | |
* | | Fixing #167.Gravatar Pierre Courtieu2017-03-13
| | |
| | * extend helpspan, issue #158Gravatar Paul Steckler2017-03-09
| |/ |/|
| * elpa: Add a package file and a package.el-friendly init scriptGravatar Clément Pit--Claudel2017-03-08
| |
| * Add a FIXME in coq.elGravatar Clément Pit--Claudel2017-03-08
| |
| * Remove uses of defpgdefault in coq-abbrevGravatar Clément Pit--Claudel2017-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 uses of defpacustom in coq-compile-commonGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | | | 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!")
| * easycrypt: Don't require pg-custom: it breaks compilationGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | | | 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.
| * Remove compile-time calls to proof-ready-for-assistantGravatar Clément Pit--Claudel2017-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'Gravatar Clément Pit--Claudel2017-03-08
| |
| * Remove a few useless eval-and-compile callsGravatar Clément Pit--Claudel2017-03-08
| |
| * Remove some Emacs <24.1 compatibility cruftGravatar Clément Pit--Claudel2017-03-08
| |
| * Fix incorrect uses of defvarGravatar Clément Pit--Claudel2017-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-compilingGravatar Clément Pit--Claudel2017-03-08
|/ | | | | The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't.
* Merge commit '06fd76163b857a056ac44e7437efa17656f06e5b'Gravatar Paul Steckler2017-03-08
|\
| * Fixing unicode tokens in generic code and in coq.Gravatar Pierre Courtieu2017-03-08
| |
* | get threeb frames only when neededGravatar Paul Steckler2017-03-06
| |
* | one more redundant call removedGravatar Paul Steckler2017-03-06
| |
* | remove redundant calls, simplify codeGravatar Paul Steckler2017-03-06
| |
* | Merge pull request #163 from ProofGeneral/fix_indentationGravatar Pierre Courtieu2017-03-03
|\ \ | | | | | | Fix indentation
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 02:16:14 +0000