diff options
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -1208,7 +1208,7 @@ be called and no command will be sent to Coq." ;; If user issued a printing option then t printing. (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) - (if coq-show-proof + (if coq-show-proof-stepwise (or (when (eq coq-diffs 'off) (list "Show." "Show Proof." )) (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs.")) @@ -1221,7 +1221,7 @@ be called and no command will be sent to Coq." (> (length coq-last-but-one-proofstack) coq--retract-naborts))) ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs (list "Unset Silent." (if (coq--post-v810) (coq-diffs) - (if coq-show-proof + (if coq-show-proof-stepwise ((when (eq coq-diffs 'off) "Show." "Show Proof." ) (when (eq coq-diffs 'on) @@ -1240,7 +1240,7 @@ be called and no command will be sent to Coq." ;; If doing (not closing) a proof, Show Proof if need be (and (not (string-match-p coq-save-command-regexp-strict cmd)) (> (length coq-last-but-one-proofstack) 0) - (when coq-show-proof + (when coq-show-proof-stepwise (list "Show." "Show Proof."))))))) @@ -1910,7 +1910,7 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-save-command "Save %s. " proof-find-theorems-command "Search %s. ") - (setq proof-show-diffs-regexp coq-show-diffs-regexp) + (setq proof-show-proof-diffs-regexp coq-show-proof-diffs-regexp) (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command) |