| Commit message (Collapse) | Author | Age |
... | |
| |
| |
| |
| | |
If this works we should probably change the generic function as well.
|
| | |
|
| | |
|
|/ |
|
| |
|
|
|
|
|
| |
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
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
The code uses several token searcher and the wrong one was called
somewhere.
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
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!")
|
| |
| |
| |
| |
| | |
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.
|
|/
|
|
|
| |
The PG Makefile does ensure (using --batch) that noninteractive is non-nil while
compiling, but package.el doesn't.
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\ \
| | |
| | | |
Fix indentation
|
| | |
| | |
| | |
| | |
| | | |
* Close ProofGeneral/PG#161.
Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open).
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- 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
|
| |/
|/| |
|
|/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
| |
- infrastructure for saving/resetting customizations not defined
with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual
|
|
|
|
|
|
| |
Split coq-par-emergency-cleanup into two functions, one for
reacting on user interrupts and one for cleaning up after
compilation errors.
|
|
|
|
| |
@psteckler I believe you have this patch already in your branch.
|
| |
|
|\
| |
| | |
Add Context to coq-syntax.el
|
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| |
| |
| |
| |
| | |
cancel-timer does of course not set the variable that holds the
timer to nil
|
|\ \
| | |
| | | |
die gracefully when visiting files in nonexisting directories
|
| | | |
|
| | | |
|
|\ \ \
| | | |
| | | | |
Add Set Printing Universes to options menu
|
| |/ /
|/| | |
|