From 057fb82fdb116ace1b3f489af3282f87fbf6a6a8 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 26 Jul 2019 16:44:15 +0000
Subject: fix: corner case where "Show." was not triggered.

Coq script example to reproduce:

--8<---------------cut here---------------start------------->8---
Set Nested Proofs Allowed.
Lemma foo : True /\ 1 = 1.
  split.              (*2*)
  easy.
  Goal True /\ 2 = 2. (*1-bug*)
  Proof.              (*1-ok*)

  split; easy.
  Qed.
  easy.
Qed.
--8<---------------cut here---------------end--------------->8---

1. goto-point (*1-bug*) (just before the comment)
2. goto-point (*2*) (bug: the goal is not shown)

3. goto-point (*1-ok*) (just after "Proof.")
4. goto-point (*2*) (no bug)
---
 coq/coq.el | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'coq')

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
-- 
cgit v1.2.3