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.

1 files changed, 3 insertions, 0 deletions

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