diff --git a/coq/coq.el b/coq/coq.el
index 71112fc1b..0243f029e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -661,7 +661,7 @@ If locked span already has a state number, then do nothing. Also updates
 ;; This hook seems the one we want.
 ;; WARNING! It is applied once after each command PLUS once before a group of
 ;; commands is started
-(add-hook 'proof-state-change-hook #'coq-set-state-infos)
+(add-hook 'proof-state-change-pre-hook #'coq-set-state-infos)
 
 
 (defun count-not-intersection (l notin)
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 14fcdcac6..b6a1b363c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1771,6 +1771,15 @@ This hook is used within Proof General to refresh the toolbar."
   :type '(repeat function)
   :group 'proof-shell)
 
+
+(defcustom proof-state-change-pre-hook nil
+  "Things to do before proof-done-advancing.
+
+E.g. classify spans by looking at the prompt."
+  :type '(repeat function)
+  :group 'proof-shell)
+
+
 ;;;;;;
 (defcustom proof-dependencies-system-specific nil
   "Set this variable to handle system specific dependency output.
@@ -1787,7 +1796,6 @@ same type as `proof-dependency-in-span-context-menu' returns."
   :type '(repeat function)
   :group 'proof-shell)
 ;;;;;
-
 (defcustom proof-shell-syntax-table-entries nil
   "List of syntax table entries for proof script mode.
 A flat list of the form
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 761a3bbe9..a5109be7c 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1382,6 +1382,8 @@ Argument SPAN has just been processed."
     (if (span-live-p proof-queue-span)
 	(proof-set-queue-start end))
 
+    (run-hooks 'proof-state-change-pre-hook)
+
     (cond
      ;; CASE 1: Comments just get highlighted
      ((eq (span-property span 'type) 'comment)
@@ -2120,6 +2122,7 @@ which is true for some proof assistants (but probably not others)."
 	(span-delete span)
 	(if killfn (funcall killfn start end))))
   ;; State of scripting may have changed now
+  (run-hooks 'proof-state-change-pre-hook)
   (run-hooks 'proof-state-change-hook))
 
 (defun proof-setup-retract-action (start end proof-commands remove-action &optional
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index a0e80fa70..c9077183c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1833,6 +1833,7 @@ If TIMEOUTSECS is a number, time out after that many seconds."
 (defun proof-done-invisible (span)
   "Callback for ‘proof-shell-invisible-command’.
 Call ‘proof-state-change-hook’."
+  (run-hooks 'proof-state-change-pre-hook)
   (run-hooks 'proof-state-change-hook))
 
 ;;;###autoload