| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
By renaming the arg load-path into loadpath I notice that a
coq-load-path was used instead of it.
|
| |\
| |
| | |
Make coq-prog-args safe when list of strings.
|
| | | |
|
| | | |
|
| |/
|
|
| |
They could be passed through _CoqProject regardless.
|
| | |
|
| |
|
|
| |
This fixes a bunch of compilation warnings
|
| |
|
|
|
| |
Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
While fixing these I discovered several flaws in indentation (what a
suprise). The probem is the following: since we don't have a precise
grammar of tactics, smie often decides that the parent of a sub-part
of a tactic is the previous command instead of the current tacic.
Typical example (fixed now but in general):
foo.
apply bar
with bar'.
Since "apply ... bar'" is considered as one leaf of the grammar, it is
considered to be a child of the previous dot.
.
/\
/ \
foo apply...bar'
Therefore indentation of "with" wants to align with parent "." and
hence with "foo".
Basically we should try to define a much more precise grammar of
complex tactics (with with, as, using etc) in order to fix the
problem. Of course this has the drawback of making impossible to
support user tactic notations.
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| |\
| |
| | |
Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
|
| | | |
|
| | |
| |
| |
| | |
when asking for it.
|
| |/ |
|
| |
|
|
|
|
|
| |
- coq--pre-v85 signals coq-unclassifiable-version for "Invalid
version" errors
- background compilation converts this into an even more helpful
message (fixes #70)
|
| |
|
|
| |
- fixes #92
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
Rationale: if Coq isn't installed, we will detect it when trying to run
it, and we don't need to duplicate the error logic.
Additionally, change from using process-lines to using shell-command,
possibly through file-name-handler. The reason for this change is that
we want to do the version detection on the remote server if we're
running in Tramp.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
Pierre Courtieu
Erik Martin-Dorel
Tej Chajed
Gaëtan Gilbert
Paul Steckler
Clément Pit--Claudel
Hendrik Tews
Pierre Courtieu