From 6d1f608c6e7c39eff89b9461a2f4ea7ff1b19899 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 14 Jan 2017 23:27:24 +0100 Subject: 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. --- generic/proof-tree.el | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'generic') 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 -- cgit v1.2.3