diff --git a/coq/coq.el b/coq/coq.el
index ca1e36a10..71112fc1b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -614,6 +614,11 @@ and read by function `coq-empty-action-list-command'.")
 
 ;;TODO update docstring and comment
 
+(defun coq-open-goals-p ()
+  "Return non nil if we are inside a proof, see `proof-shell-open-goals-p'."
+  (car (cdr (cdr (coq-last-prompt-info-safe)))))
+
+
 (defun coq-set-state-infos ()
   "Set the last locked span's state number to the number found last time.
 This number is in the *last but one* prompt (variable `coq-last-but-one-statenum').
@@ -1897,6 +1902,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
           coq-compile-auto-save coq-lock-ancestors coq-diffs))
 
   (setq proof-goal-command-p #'coq-goal-command-p
+        proof-shell-last-cmd-left-goals-p #'coq-open-goals-p
         proof-find-and-forget-fn #'coq-find-and-forget
         pg-topterm-goalhyplit-fn #'coq-goal-hyp
         proof-state-preserving-p #'coq-state-preserving-p)
diff --git a/generic/proof-config.el b/generic/proof-config.el
index c10c0ee0d..14fcdcac6 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1499,6 +1499,19 @@ on `proof-shell-eager-annotation-start' and
   :type '(choice (const nil) regexp)
   :group 'proof-shell)
 
+(defcustom proof-shell-last-cmd-left-goals-p nil
+  "A function to test: are we currently inside a proof?
+
+This function takes no argument and should use
+`proof-shell-last-prompt' and `proof-shell-last-output' to
+determine whether the last command ended up inside a
+proof (either by remaining inside one or opening a new one), or
+outside of any proof.
+"
+  :type 'function
+  :group 'proof-script)
+
+
 
 ;;
 ;; 3c. tokens mode: turning on/off tokens output