clear goals buffer after Qed and Admitted when running silent

This solves the remaining known problems from #568. Fixes #568.

Author: hendriktews

ci/simple-tests/coq-test-goals-present.el

@@ -280,7 +280,6 @@ which action the goals buffer should have been reset."
 
 (ert-deftest goals-reset-after-admitted ()
   "The goals buffer is reset after an Admitted."
-  :expected-result :failed
   (goals-buffer-should-get-reset coq-src-admitted "intros P" "Admitted"))
 
 (ert-deftest goals-reset-no-more-goals ()
@@ -289,7 +288,6 @@ which action the goals buffer should have been reset."
                                  "Lemma a" "no more goals"))
 
 (ert-deftest goals-reset-qed ()
-  :expected-result :failed
   "The goals buffer is reset after Qed."
   (goals-buffer-should-get-reset coq-src-qed
                                  "Proof using" "Qed"))

coq/coq.el

@@ -3213,8 +3213,15 @@ number of hypothesis displayed, without hiding the goal"
                                     (coq-build-subgoals-string nbgoals nbunfocused)))
                         minor-mode-alist)))))))
 
-
-
+(defun coq-clean-goals-outside-proof ()
+  "Clear goals buffer outside proofs.
+This function ensures that the goals buffer is reset after Qed or
+Admitted. This function is for
+`proof-shell-handle-delayed-output-hook'."
+  (when (or (not coq-last-but-one-proofstack)
+            (proof-string-match coq-shell-proof-completed-regexp
+                                proof-shell-last-output))
+    (proof-clean-buffer proof-goals-buffer)))
 
 
 ;; This hook must be added before coq-optimise-resp-windows, in order to be evaluated
@@ -3224,10 +3231,7 @@ number of hypothesis displayed, without hiding the goal"
 (add-hook 'proof-shell-handle-delayed-output-hook
 	  #'coq-update-minor-mode-alist)
 (add-hook 'proof-shell-handle-delayed-output-hook
-          (lambda ()
-            (if (proof-string-match coq-shell-proof-completed-regexp
-                                    proof-shell-last-output)
-                (proof-clean-buffer proof-goals-buffer))))
+          #'coq-clean-goals-outside-proof)
 
 (add-hook 'proof-shell-handle-delayed-output-hook
 	  (lambda ()