First try for feature #487

1 files changed, 8 insertions, 1 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 71112fc1..8ebf3054 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1222,7 +1222,14 @@ be called and no command will be sent to Coq."
      (string-match-p "BackTo\\s-" cmd))
     (if (coq--post-v810)
         (list "Unset Silent." (coq-diffs))
-      (list "Unset Silent.")))))
+      (list "Unset Silent.")))
+   ((or
+     ;; 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
+            (list  "Show Proof." "Show.")))))))
+
 
 (defpacustom auto-adapt-printing-width t
   "If non-nil, adapt automatically printing width of goals window.