diff --git a/coq/coq.el b/coq/coq.el
index efa603499..8b9cec69d 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -671,7 +671,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/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 5740faa20..14fe5219e 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -3107,7 +3107,8 @@ before and after sending the command.
 In case @var{cmd} is (or yields) nil, do nothing.
 
 @var{invisiblecallback} will be invoked after the command has finished,
-if it is set.  It should probably run the hook variables
+if it is set. It should probably run the hook variables
+@samp{@code{proof-state-change-pre-hook}} and
 @samp{@code{proof-state-change-hook}}.
 
 @var{flags} are additional flags to put onto the @samp{@code{proof-action-list}}.
@@ -4056,8 +4057,9 @@ not need to use these directly.
 @c TEXI DOCSTRING MAGIC: proof-grab-lock
 @defun proof-grab-lock &optional queuemode
 Grab the proof shell lock, starting the proof assistant if need be.@*
-Runs @samp{@code{proof-state-change-hook}} to notify state change.
-If @var{queuemode} is supplied, set the lock to that value.
+Runs @samp{@code{proof-state-change-pre-hook}} and
+@samp{@code{proof-state-change-hook}} to notify state change. If
+@var{queuemode} is supplied, set the lock to that value.
 @end defun
 
 @c TEXI DOCSTRING MAGIC: proof-release-lock
diff --git a/easycrypt/easycrypt-hooks.el b/easycrypt/easycrypt-hooks.el
index 675929739..376936f61 100644
--- a/easycrypt/easycrypt-hooks.el
+++ b/easycrypt/easycrypt-hooks.el
@@ -68,7 +68,7 @@
        (setq easycrypt-proof-weak-mode (car (cdr infos)))
      )))
 
-(add-hook 'proof-state-change-hook 'easycrypt-set-state-infos)
+(add-hook 'proof-state-change-pre-hook 'easycrypt-set-state-infos)
 
 (defun easycrypt-find-and-forget (span)
   (let ((span-staten (easycrypt-get-span-statenum span)))
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 9d3525489..6f1e91487 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1766,16 +1766,35 @@ symbol is 'systemspecific."
   :type '(repeat function)
   :group 'proof-shell)
 
+
+(defcustom proof-state-change-pre-hook nil
+  "This hook is called when a scripting state change may have occurred.
+Specifically, this hook is called after a region has been asserted or
+retracted, or after a command has been sent to the prover with
+`proof-shell-invisible-command'.
+
+It is run *before* the generic processing of the command span is
+done (see function `prof-done-advancing'). See
+`proof-state-change-hook' to insert actions after it."
+  :type '(repeat function)
+  :group 'proof-shell)
+
 (defcustom proof-state-change-hook nil
   "This hook is called when a scripting state change may have occurred.
 Specifically, this hook is called after a region has been asserted or
 retracted, or after a command has been sent to the prover with
 `proof-shell-invisible-command'.
 
-This hook is used within Proof General to refresh the toolbar."
+It is run *after* the generic processing of the command span is
+done (see function `prof-done-advancing'). See
+`proof-state-change-pre-hook' to insert actions before it.
+
+This hook may be used to refresh the toolbar."
   :type '(repeat function)
   :group 'proof-shell)
 
+
+
 ;;;;;;
 (defcustom proof-dependencies-system-specific nil
   "Set this variable to handle system specific dependency output.
@@ -1792,7 +1811,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 b9ac2b3cf..78b36ee70 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -243,6 +243,7 @@ If QUEUEMODE is supplied, set the lock to that value."
   (setq proof-shell-interrupt-pending nil
 	proof-shell-busy (or queuemode t)
 	proof-shell-last-queuemode proof-shell-busy)
+  (run-hooks 'proof-state-change-pre-hook)
   (run-hooks 'proof-state-change-hook))
 
 (defun proof-release-lock ()
@@ -1836,6 +1837,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
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index c7afe2128..1a01147b7 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -814,6 +814,7 @@ call `proof-tree-make-show-goal-callback', which evaluates to a
 lambda expressions that you can put into `proof-action-list'."
   ;;(message "PTSGC %s" state)
   (proof-tree-update-sequent state)
+  (run-hooks 'proof-state-change-pre-hook)
   (run-hooks 'proof-state-change-hook))
 
 (defun proof-tree-make-show-goal-callback (state)