| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
This fixes a bunch of compilation warnings
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
|
|
|
| |
- protocol change, but stay at version 3
|
|
|
|
| |
- prooftree protocol change to version 3
|
| |
|
| |
|
|
|
|
|
|
| |
* protocol change
- rename proof-complete into proof-finished and add existential info
- add proof-complete message
|
|
- add support for proof-tree displays (currently Coq only)
- new file generic/proof-tree.el contains generic code
- Coq specific code has been added to coq/coq.el
Changes to existing Proof General functions:
- proof-shell-exec-loop and proof-shell-filter-manage-output call
proof-tree display functions, when the proof-tree display is on
- proof-shell-exec-loop returns t if proof-action-list is empty
_or_ contains only items for updating the proof-tree
- proof-shell-should-be-silent returns nil when the proof-tree
display is on
- coq-last-prompt-info, coq-last-prompt-info-safe return as
additional 4th element the name of the current proof
|