1 files changed, 1 insertions, 2 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 20646083..6ccb7ffc 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1213,8 +1213,7 @@ be called and no command will be sent to Coq."
      ;; If we go back in the buffer and the number of abort is less than
      ;; the number of nested goals, then Unset Silent and Show the goal
      (and (string-match-p "BackTo\\s-" cmd)
-          (> (length (coq-get-span-proofstack (proof-last-locked-span)))
-             coq--retract-naborts)))
+          (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
     ; "Set Diffs" always re-prints the proof context with (if enabled) diffs
     (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")))
    ((or