diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2017-01-14 23:27:24 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2017-01-14 23:31:01 +0100 |
| commit | 6d1f608c6e7c39eff89b9461a2f4ea7ff1b19899 (patch) | |
| tree | 44804b5266e056b900a9ecc7e03c1f5a34a89992 /generic | |
| parent | 15b977ff32f6c8250d47d7657987b0c94db76710 (diff) | |
Fix prooftree for Coq 8.6
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.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-tree.el | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 77d3cc33..f0894656 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -842,13 +842,14 @@ The not yet delayed output is in the region (start proof-shell-delayed-output-start) (end proof-shell-delayed-output-end) inst-ex-vars) - (when (and (not (memq 'proof-tree-show-subgoal flags)) - (> state proof-tree-last-state)) - ;; Only deal with existentials if the proof assistant has them - ;; (i.e., proof-tree-existential-regexp is set) and if there are some - ;; goals with existentials. - (when (and proof-tree-existential-regexp + (unless (memq 'proof-tree-show-subgoal flags) + (when (and (> state proof-tree-last-state) + proof-tree-existential-regexp proof-tree-existentials-alist) + ;; Only deal with existentials if this is not and undo + ;; command, if the proof assistant actually has existentials + ;; (i.e., proof-tree-existential-regexp is set) and if there + ;; are some goals with existentials. (setq inst-ex-vars (with-current-buffer proof-shell-buffer (funcall proof-tree-extract-instantiated-existentials |