coq: clear goals buffer after admitted

Author: hendriktews

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

@@ -174,7 +174,6 @@ goals buffer is not empty afterwards."
   (goals-after-test coq-src-error "error"))
 
 (ert-deftest goals-reset-after-admitted ()
-  :expected-result :failed
   "The goals buffer is reset after an Admitted."
   (message
    "goals-reset-after-admitted: Check that goals are reset after Admitted.")

coq/coq.el

@@ -145,8 +145,17 @@ Namely, goals that do not fit in the goals window."
 ;;  "Add LoadPath \"%s\"." ;; fixes unadorned Require (if .vo exists).
   "*Command of the inferior process to change the directory.")
 
-(defvar coq-shell-proof-completed-regexp "No\\s-+more\\s-+\\(?:sub\\)?goals\\.\\|Subtree\\s-proved!\\|Proof\\s-completed"; \\|This subproof is complete
-  "*Regular expression indicating that the proof has been completed.")
+(defvar coq-shell-proof-completed-regexp
+  (concat "No\\s-+more\\s-+\\(?:sub\\)?goals\\.\\|Subtree\\s-proved!\\|"
+          "Proof\\s-completed\\|.*\\s-is\\s-declared"
+          ;; \\|This subproof is complete
+          )
+  "*Regular expression indicating that the proof has been completed.
+Coq instance of `proof-shell-clear-goals-regexp'. Used in
+`proof-shell-process-urgent-message' to determine if the goals
+buffer shall be cleaned. Some of the messages recognized here are
+not printed by Coq in silent mode, such that Proof General might
+fail to delete the goals buffer.")
 
 (defvar coq-goal-regexp
   "\\(============================\\)\\|\\(\\(?:sub\\)?goal [0-9]+\\)\n")

generic/proof-shell.el

@@ -35,6 +35,7 @@
 ;;   proof-shell-filter-wrapper
 ;;   -> proof-shell-filter
 ;;      -> proof-shell-process-urgent-messages
+;;         -> proof-shell-process-urgent-message
 ;;      -> proof-shell-filter-manage-output
 ;;         -> proof-shell-handle-immediate-output
 ;;         -> proof-shell-exec-loop