aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-17Disable ASLR during Travis buildsClément Pit--Claudel
2018-01-16Get rid of old-style backquotesClément Pit--Claudel
Closes #221. Thanks @jwiegley!
2018-01-15Experimental fix for #220.Pierre Courtieu
2017-12-22Make coq-prog-args safe when list of strings.Gaëtan Gilbert
They could be passed through _CoqProject regardless.
2017-12-11Fix #214.Pierre Courtieu
If this works we should probably change the generic function as well.
2017-11-06Prettier cheat face (background + box).Pierre Courtieu
2017-11-06Fix #135.Pierre Courtieu
2017-10-26Updating CHANGES with lexer extensibility.Pierre Courtieu
2017-10-26Limited extensibility of smie token detection.Pierre Courtieu
2017-09-22phox syntax table + more symbolsChristophe Raffalli
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-07-19changed -emacs-U flag to -emacsPaul Steckler
2017-07-06Merge pull request #191 from AndreasLoow/proof-layout-windows-doc-formattingPierre Courtieu
Formatting fix for proof-layout-windows documentation
2017-06-30Formatting fix for proof-layout-windows documentationAndreas Lööw
2017-06-19Merge pull request #189 from marsam/masterClément Pit-Claudel
Fix easycrypt automode regexp
2017-06-19Fix easycrypt automode regexpMario Rodas
Without the string-end regexp matches all the file names which match the regexp `.eca?`.
2017-06-08Fixing 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-06Adding 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-06Fixing bug #187 by removing trailing spaces from prog name.Pierre Courtieu
2017-05-25Merge pull request #185 from psteckler/remove-contribspsteckler
Remove mmm and ML4PG contribs
2017-05-24Remove mmm and ML4PG contribs and remove references to them in code and docsPaul Steckler
2017-05-23Fixing #183.Pierre Courtieu
2017-05-16Fixing 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-12temporary fix of automatic intros.Pierre Courtieu
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-04-25Typo 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-25Remove bin/proofgeneral and Update Makefiles accordingly.Erik Martin-Dorel
Closes ProofGeneral/PG#177
2017-04-24Preparing new warning tags (no more special chars).Pierre Courtieu
2017-04-19Fix #176.Pierre Courtieu
The code uses several token searcher and the wrong one was called somewhere.
2017-04-18Add file contrib/mmm/.nosearch to help feature extraction toolsJonas 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 modePierre-Yves Strub
2017-03-31Fixing #173.Pierre Courtieu
2017-03-22Added support for future new options (trunk).Pierre Courtieu
2017-03-13Fixing #167.Pierre Courtieu
2017-03-09extend helpspan, issue #158Paul Steckler
2017-03-08elpa: Add a package file and a package.el-friendly init scriptClément Pit--Claudel
2017-03-08Add a FIXME in coq.elClément Pit--Claudel
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 uses of defpacustom in coq-compile-commonClé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-08easycrypt: Don't require pg-custom: it breaks compilationClé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-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 a few useless eval-and-compile callsClé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-08Merge commit '06fd76163b857a056ac44e7437efa17656f06e5b'Paul Steckler
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:28:39 +0000