From f14fbab4ea3497aa51f2e44fe77a359e9b77eb24 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 28 Jan 2011 09:57:54 +0000
Subject: Clean coq goals buffer when backing to a non-proof state, otherwise
 the old goal was still displayed (and therefore the old number of goals too).
 Fixes trac #386.

---
 coq/coq.el | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/coq/coq.el b/coq/coq.el
index 255ca23f..516125a8 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -499,6 +499,9 @@ If locked span already has a state number, then do nothing. Also updates
              (span-staten (coq-get-span-statenum span))
              (naborts (count-not-intersection 
                        coq-last-but-one-proofstack proofstack)))
+    ;; if we move outside of any proof, coq does not print anything, so clean
+    ;; the goals buffer otherwise the old one will still be displayed
+    (if (= proofdepth 0) (proof-clean-buffer proof-goals-buffer))
     (unless (and 
              ;; return nil (was proof-no-command) in this case:
              ;; this is more efficient as backtrack x y z may be slow
-- 
cgit v1.2.3