| Commit message (Collapse) | Author | Age |
... | |
|\ \ \ \
| | | | |
| | | | | |
Update copyright messages and improve the header of elisp files.
|
|/ / / / |
|
| | | |
| | | |
| | | | |
Close ProofGeneral/PG#31
|
| | | | |
|
|\ \ \ \
| | | | |
| | | | | |
Look for vernac controls before focus bracket, possible fix for #223
|
|/ / / / |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | | |
Closes #221. Thanks @jwiegley!
|
| | | | |
|
| | | |
| | | |
| | | |
| | | | |
They could be passed through _CoqProject regardless.
|
| | | |
| | | |
| | | |
| | | | |
If this works we should probably change the generic function as well.
|
| | | | |
|
| | | | |
|
| | | | |
|
|/ / / |
|
| | | |
|
|/ / |
|
| |
| |
| |
| | |
This commit address ProofGeneral/PG#193.
|
| | |
|
|\ \
| | |
| | | |
Formatting fix for proof-layout-windows documentation
|
|/ / |
|
|\ \
| | |
| | | |
Fix easycrypt automode regexp
|
|/ /
| |
| |
| |
| | |
Without the string-end regexp matches all the file names which match the regexp
`.eca?`.
|
| |
| |
| |
| |
| | |
The "Show" inserted now and then would hide the result of Set/Unset
commands.
|
| |
| |
| |
| |
| | |
Checking whether the backtrack is inside a proof or not is a bit
convoluted but seems ok.
|
| | |
|
|\ \
| | |
| | | |
Remove mmm and ML4PG contribs
|
| | | |
|
|/ / |
|
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| |
| |
| |
| | |
This fixes a bunch of compilation warnings
|
|\ \
| | |
| | | |
[WIP] ELPA/MELPA support
|
| | | |
|
| | |
| | |
| | | |
This commit contributes to shorten the real time of Travis' automated build.
|
| | |
| | |
| | |
| | | |
Closes ProofGeneral/PG#177
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
The code uses several token searcher and the wrong one was called
somewhere.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/
|/| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
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'.
|
| |
| |
| |
| |
| |
| | |
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!")
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| | |
Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.
|