fix: Do "Show Proof…" (with "?Goal") as soon as the proof is started

1 files changed, 4 insertions, 2 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 942e85fe..10aa07bf 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1246,14 +1246,16 @@ be called and no command will be sent to Coq."
         (list "Unset Silent." (coq-diffs) )
       (list "Unset Silent.")))
    ((or
+     ;; If starting a proof, Show Proof if need be
+     (coq-goal-command-str-p cmd)
      ;; 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)
+          (> (length coq-last-but-one-proofstack) 0)))
           (when coq-show-proof-stepwise
               (or
     (when (eq coq-diffs 'off) (list "Show Proof." ))
     (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
-    (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))))
+    (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))
 
 
 (defpacustom auto-adapt-printing-width t