From 411ebb27fda4d39fc22baf341dcdde2341632b8d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 20 May 2020 21:48:20 +0200
Subject: fix: Do "Show Proof…" (with "?Goal") as soon as the proof is started

---
 coq/coq.el | 6 ++++--
 1 file 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
-- 
cgit v1.2.3