diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 7f4291b16..d911f6e21 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -196,6 +196,8 @@ For example, COMMENT could be (*test-definition*)"
 
 
 (ert-deftest 020_coq-test-definition ()
+  ;; There are no infomsgr when running silent.
+  :expected-result :failed
   "Test *response* output after asserting a Definition."
   (coq-fixture-on-file
    (coq-test-full-path "test_stepwise.v")
@@ -317,6 +319,10 @@ For example, COMMENT could be (*test-definition*)"
  
 
 (ert-deftest 090_coq-test-regression-Fail()
+  ;; When running silent, the message about indeed failing is not
+  ;; shown. One might fix this test by checking that there is no
+  ;; error, which would be shown without Fail.
+  :expected-result :failed
   "Test for Fail"
   (coq-fixture-on-file
    (coq-test-full-path "test_stepwise.v")
@@ -338,6 +344,13 @@ Tactic failure: Cannot solve this goal." "*coq*")))))
 ;; (coq-should-buffer-regexp (regexp-quote "The command has indeed failed with message: Tactic failure: Cannot solve this goal.") "*response*")
 
 (ert-deftest 091_coq-test-regression-Fail()
+  ;; XXX What is the difference between this test and
+  ;; 090_coq-test-regression-Fail?
+
+  ;; When running silent, the message about indeed failing is not
+  ;; shown. One might fix this test by checking that there is no
+  ;; error, which would be shown without Fail.
+  :expected-result :failed
   "Test for Fail"
   (coq-fixture-on-file
    (coq-test-full-path "test_stepwise.v")
diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el
index e0784f1ba..d0a3fc0cf 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -67,13 +67,33 @@ Proof using.
   "Coq source code for checking goals after an error.")
 
 (defconst coq-src-admitted
-  "Lemma a : forall(P27X : Prop), P27X.
+  "Lemma a : forall(P : Prop), P.
 Proof using.
-  intros P27X.
+  intros P.
   Admitted.
 "
   "Coq source for checking that the goals buffer is reset after Admitted.")
 
+(defconst coq-src-no-more-goals
+  "
+Lemma a : 1 + 1 = 2.
+Proof using.
+  simpl.
+  auto.
+"
+  "Coq source code for checking that the goals buffer is reset when
+no goals are left.")
+
+(defconst coq-src-qed
+  "
+Lemma a : 1 + 1 = 2.
+Proof using.
+  simpl.
+  auto.
+Qed.
+"
+  "Coq source code for checking that the goals buffer is reset after Qed.")
+
 (defconst coq-src-update-goal-after-error
   "
 (* code taken from pull request #429 *)
@@ -121,10 +141,12 @@ BUF should be a string."
 
 ;;; define the tests
 
-(defun goals-after-test (coq-src msg)
+(defun goals-after-test (coq-src msg check-response-nonempty)
   "Test that Proof General shows goals after processing COQ-SRC.
 Process COQ-SRC in a new buffer in one step and check that the
-goals buffer is not empty afterwards."
+goals buffer is not empty afterwards. If CHECK-RESPONSE-NONEMPTY
+is non-nil, additionally check that the response buffer is
+non-empty, i.e., shows some error message."
   (message "goals-after-test: Check goals are present after %s." msg)
   (setq proof-three-window-enable nil)
   (let (buffer)
@@ -141,78 +163,114 @@ goals buffer is not empty afterwards."
           ;; check that there is a goal in the goals buffer
           (with-current-buffer "*goals*"
             (goto-char (point-min))
-            (should (looking-at "1 \\(sub\\)?goal (ID"))))
+            (should (looking-at "1 \\(sub\\)?goal (ID")))
+
+          (when check-response-nonempty
+            (message
+             "goals-after-test: Check response buffer is nonempty after %s."
+             msg)
+            (with-current-buffer "*response*"
+              (should (not (equal (point-min) (point-max)))))))
+
+      ;; clean up
+      (when buffer
+        (with-current-buffer buffer
+          (set-buffer-modified-p nil))
+        (kill-buffer buffer)))))
+
+(defun goals-buffer-should-be-empty (pos msg)
+  "Check that `*goals*' is empty after asserting/retracting to POS.
+MSG is only used in a message, it should tell after which action
+the goals buffer is expected to be empty."
+  (message "Check that goals buffer is empty after %s" msg)
+  (goto-char pos)
+  (proof-goto-point)
+  (wait-for-coq)
+  ;; (record-buffer-content "*coq*")
+  ;; (record-buffer-content "*goals*")
+
+  ;; check that the goals buffer is empty
+  (with-current-buffer "*goals*"
+    (should (equal (point-min) (point-max)))))
+
+(defun goals-buffer-should-get-reset (coq-src coq-stm msg)
+  "Check that the goals buffer is reset.
+Put the string COQ-SRC into a buffer and assert until the first
+occurrence of COQ-STM, which should be a regular expression. At
+this point the goals buffer needs to contain something. Then
+assert to the end of COQ-SRC and check that the goals buffer has
+been reset. MSG is used in messages only. It shouls say after
+which action the goals buffer should have been reset."
+  (message "Check that goals are reset after %s." msg)
+  (setq proof-three-window-enable nil)
+  (let (buffer)
+    (unwind-protect
+        (progn
+          (find-file "goals.v")
+          (setq buffer (current-buffer))
+          (insert coq-src)
+
+          ;; First fill the goals buffer by asserting until the line
+          ;; after the first occurrence of COQ-STM.
+
+          (goto-char (point-min))
+          (should (re-search-forward coq-stm nil t))
+          (forward-line 1)
+          (message "*goals* should be non-empty after asserting until after %s"
+                   coq-stm)
+          (proof-goto-point)
+          (wait-for-coq)
+          ;; there should be something in the goals buffer now
+          (with-current-buffer "*goals*"
+            (should (not (equal (point-min) (point-max)))))
+
+          (goals-buffer-should-be-empty (point-max) msg))
 
       ;; clean up
       (when buffer
         (with-current-buffer buffer
           (set-buffer-modified-p nil))
         (kill-buffer buffer)))))
+  
 
 (ert-deftest goals-after-proof ()
   "Test goals are present after ``Proof''."
-  :expected-result (if coq--post-v87 :failed :passed)
-  (goals-after-test coq-src-proof "Proof"))
+  (goals-after-test coq-src-proof "Proof" nil))
 
 (ert-deftest goals-after-comment ()
   "Test goals are present after a comment."
-  :expected-result :failed
-  (goals-after-test coq-src-comment "comment"))
+  (goals-after-test coq-src-comment "comment" nil))
 
 (ert-deftest goals-after-auto ()
   "Test goals are present after ``auto''."
-  :expected-result  (if coq--post-v87 :failed :passed)
-  (goals-after-test coq-src-auto "auto"))
+  (goals-after-test coq-src-auto "auto" nil))
 
 (ert-deftest goals-after-simpl ()
   "Test goals are present after ``simpl''."
-  (goals-after-test coq-src-simpl "simpl"))
+  (goals-after-test coq-src-simpl "simpl" nil))
 
 (ert-deftest goals-after-error ()
   "Test goals are present after an error."
-  :expected-result :failed
-  (goals-after-test coq-src-error "error"))
+  (goals-after-test coq-src-error "error" t))
 
 (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.")
-  (setq proof-three-window-enable nil)
-  (let (buffer)
-    (unwind-protect
-        (progn
-          (find-file "goals.v")
-          (setq buffer (current-buffer))
-          (insert coq-src-admitted)
-
-          ;; Need to assert the Admitted alone, therefore first assert
-          ;; until before the Admitted.
-          (goto-char (point-min))
-          (should (re-search-forward "intros P27X" nil t))
-          (forward-line 1)
-          (proof-goto-point)
-          (wait-for-coq)
+  (goals-buffer-should-get-reset coq-src-admitted "intros P" "Admitted"))
 
-          (forward-line 1)
-          (proof-goto-point)
-          (wait-for-coq)
-          ;; (record-buffer-content "*coq*")
-          ;; (record-buffer-content "*goals*")
+(ert-deftest goals-reset-no-more-goals ()
+  "The goals buffer is reset when there are no more goals."
+  (goals-buffer-should-get-reset coq-src-no-more-goals
+                                 "Proof using" "no more goals"))
 
-          ;; check that the old goal is not present in the goals buffer
-          (with-current-buffer "*goals*"
-            (goto-char (point-min))
-            (should (not (re-search-forward "P27X" nil t)))))
-
-      ;; clean up
-      (when buffer
-        (with-current-buffer buffer
-          (set-buffer-modified-p nil))
-        (kill-buffer buffer)))))
+(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"))
 
 (ert-deftest update-goals-after-error ()
   "Test goals are updated after an error."
-  :expected-result :failed
   (message "update-goals-after-error: Check goals are updated after error")
   (setq proof-three-window-enable nil)
   (let (buffer)
@@ -230,6 +288,7 @@ goals buffer is not empty afterwards."
           ;; (record-buffer-content "*goals*")
 
           ;; the complete goal should be present
+          (message "Check that the complete goal is present in *goals*")
           (with-current-buffer "*goals*"
             (goto-char (point-min))
             (should (re-search-forward "(eq_one 1 -> False) -> False" nil t)))
@@ -242,9 +301,16 @@ goals buffer is not empty afterwards."
           ;; (record-buffer-content "*goals*")
 
           ;; the hypothesis H should be present
+          (message "Check that the goals buffer has been updated")
           (with-current-buffer "*goals*"
             (goto-char (point-min))
-            (should (re-search-forward "H : eq_one 1 -> False" nil t))))
+            (should (re-search-forward "H : eq_one 1 -> False" nil t)))
+
+          ;; some error should be in the response buffer
+          (message "Check that there is some error message present")
+          (with-current-buffer "*response*"
+            (should (not (equal (point-min) (point-max))))))
+
       (when buffer
         (with-current-buffer buffer
           (set-buffer-modified-p nil))
diff --git a/coq/coq.el b/coq/coq.el
index a036acde3..a6446a174 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -122,8 +122,21 @@ Namely, goals that do not fit in the goals window."
      ;; should re-intialize to coq-search-blacklist-string instead of
      ;; keeping the current value (that may come from another file).
      ,(format "Add Search Blacklist %s. " coq-search-blacklist-current-string))
-   '("Set Suggest Proof Using. ") coq-user-init-cmd)
-  "Command to initialize the Coq Proof Assistant.")
+   '("Set Suggest Proof Using. "
+     "Set Silent. ")
+   coq-user-init-cmd)
+  "Commands for initial Coq configuration, Coq variant of `proof-shell-init-cmd'.
+List of commands sent to the Coq background process just after it
+has been started. This happens inside `proof-shell-config-done',
+when the major mode `coq-shell-mode' is configured in the `*coq*'
+buffer.
+
+Sets silent mode.
+
+In normal interaction, Coq is started because the user assert
+some commands. Therefore the commands here are followed by those
+inserted inside `proof-assert-command-hook', respectively,
+`coq-adapt-printing-width'.")
 
 ;; FIXME: Even if we don't use coq-indent for indentation, we still need it for
 ;; coq-script-parse-cmdend-forward/backward and coq-find-real-start.
@@ -1207,12 +1220,18 @@ Printing All set."
 ;; command and *not* have the goal redisplayed, the command must be tagged with
 ;; 'empty-action-list.
 (defun coq-empty-action-list-command (cmd)
-  "Return the list of commands to send to Coq after CMD
-if it is the last command of the action list.
-If CMD is tagged with 'empty-action-list then this function won't
-be called and no command will be sent to Coq.
+  "Return the list of commands to send to Coq if CMD is last in the action list.
+Return the list of commands to be sent to Coq when
+`proof-action-list' is empty, CMD was the last command just sent
+to Coq and CMD was not tagged with `'empty-action-list'.
 Note: the last command added if `coq-show-proof-stepwise' is set
-should match the `coq-show-proof-diffs-regexp'."
+should match the `coq-show-proof-diffs-regexp'.
+
+When Coq runs silent, this function must return the necessary
+Show commands to fill the `*goals*' buffer inside a proof.
+
+This function is called from `proof-shell-exec-loop' via
+`proof-shell-empty-action-list-command'."
   (cond
    ((or
      ;; If closing a nested proof, Show the enclosing goal.
@@ -1221,32 +1240,39 @@ should match the `coq-show-proof-diffs-regexp'."
      ;; If user issued a printing option then t printing.
      (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
+    ;; (message "coq-empty-action-list case 1")
     `("Show."
       . ,(coq--show-proof-stepwise-cmds)))
    
    ((or
-     ;; 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
+     ;; If we go back in the buffer and the number of abort is less than the
+     ;; number of nested goals, that is, if we are inside a proof, then Show
+     ;; the goal.
      (and (string-match-p "BackTo\\s-" cmd)
           (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
-    `("Unset Silent."
-      ,(if (coq--post-v810) (coq-diffs) "Show.")
-      . ,(coq--show-proof-stepwise-cmds)))
+    ;; (message "coq-empty-action-list case 2")
+    (append
+     (if (coq--post-v810) (list (coq-diffs)) ())
+     '("Show.")
+     (coq--show-proof-stepwise-cmds)))
 
    ((or
-     ;; If we go back in the buffer and not in the above case, then only Unset
-     ;; silent (there is no goal to show). Still, we need to "Set Diffs" again
+     ;; If we go back in the buffer and not in the above case, i.e., outside a
+     ;; proof, then only set the Diffs option.
      (string-match-p "BackTo\\s-" cmd))
-    (if (coq--post-v810)
-        (list "Unset Silent." (coq-diffs) )
-      (list "Unset Silent.")))
+    ;; (message "coq-empty-action-list case 3")
+    (if (coq--post-v810) (list (coq-diffs)) ()))
+     
    ((or
      ;; If starting a proof, Show Proof if need be
      (coq-goal-command-str-p cmd)
      ;; If doing (not closing) a proof, Show Proof if need be
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
           (> (length coq-last-but-one-proofstack) 0)))
-    (coq--show-proof-stepwise-cmds))))
+    ;; (message "coq-empty-action-list case 4")
+    (append
+     '("Show.")
+     (coq--show-proof-stepwise-cmds)))))
 
 ;; This does not Set Printing Width, it rather tells pg to do that before each
 ;; command (if necessary)
@@ -1326,7 +1352,9 @@ redisplayed."
     (let ((wdth (or width (coq-guess-goal-buffer-at-next-command))))
       ;; if no available width, or unchanged, do nothing
       (when (and wdth (not (equal wdth coq-shell-current-line-width)))
-        (proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t)
+        (proof-shell-invisible-command
+         (format "Set Printing Width %S." (- wdth 1))
+         t nil 'empty-action-list)
         (setq coq-shell-current-line-width wdth)
         ;; Show iff show non nil and some proof is under way
         (when (and show (not (null (cl-caddr (coq-last-prompt-info-safe)))))
@@ -1846,7 +1874,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
           (let ((pt2 (point)))
             (re-search-backward "Goal:\\|^TcDebug\\|^</prompt>" nil t)
             (when (looking-at "Goal")
-              (pg-goals-display (buffer-substring (point) pt2) nil))))))))
+              (pg-goals-display (buffer-substring (point) pt2) nil nil))))))))
 
 ;; overwrite the generic one, interactive prompt is Debug mode;; try to display
 ;; the debug goal in the goals buffer.
@@ -1943,8 +1971,11 @@ at `proof-assistant-settings-cmds' evaluation time.")
   ;; span menu
   (setq proof-script-span-context-menu-extensions #'coq-create-span-menu)
 
-  (setq proof-shell-start-silent-cmd "Set Silent. "
-        proof-shell-stop-silent-cmd "Unset Silent. ")
+  ;; When proof-shell-start-silent-cmd and proof-shell-stop-silent-cmd stay at
+  ;; their default value nil, the generic code won't switch Coq to silent and
+  ;; noisy at, respectively, the beginning and end of longer asserted regions.
+  ;; (setq proof-shell-start-silent-cmd "Set Silent. "
+  ;;       proof-shell-stop-silent-cmd "Unset Silent. ")
 
   ;; prooftree config
   (setq
@@ -1969,6 +2000,21 @@ at `proof-assistant-settings-cmds' evaluation time.")
   )
 
 (defun coq-shell-mode-config ()
+  "Initialization of `coq-shell-mode' that runs in the `*coq*' buffer.
+The interaction buffer with Coq, `*coq*', uses a major mode that
+is derived via `proof-shell-mode' from `scomint-mode'. This
+function runs as the body of `coq-shell-mode' when the `*coq*'
+buffer is initialized, which happens when the Coq background
+process is started. This function intitalizes the Coq
+personalization of Proof General in the interaction buffer with
+Coq. At the end, this function calls `proof-shell-config-done',
+which initializes the Coq session, e.g., by sending
+`proof-shell-init-cmd', respectively, `coq-shell-init-cmd' to Coq.
+
+In normal interaction, the proof assistant is started because the
+user assert some commands. Therefore this function runs only
+shortly before `proof-assert-command-hook', respectively,
+`coq-adapt-printing-width'."
   (setq
    proof-shell-cd-cmd coq-shell-cd
    proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\""   . "\\\""))
@@ -3017,6 +3063,26 @@ buffer."
 (add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-highlight-error-hook t)
 
 
+(defun coq-show-goals-on-error ()
+  "Update goals buffer on error if necessary.
+This function is intended for
+`proof-shell-handle-error-or-interrupt-hook'. When Coq reported
+an error, this function issues a Show command to update the goals
+buffer, in case we are inside a proof. The hook is processed deep
+inside `proof-shell-filter' after the action list has been reset
+and the proof shell lock `proof-shell-busy' has been released,
+all because of the error. The Show must therefore be added as
+priority action. The flags of the action item must contain
+`'keep-response', because in two-pane mode we want to show the
+response buffer to the user."
+  (when coq-last-but-one-proofstack
+    (proof-add-to-priority-queue
+     (proof-shell-action-list-item
+      "Show. " 'proof-done-invisible
+      (list 'keep-response 'invisible 'empty-action-list)))))
+
+(add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-show-goals-on-error)
+
 ;;
 ;; Scroll response buffer to maximize display of first goal
 ;;
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 3e5e72e39..5fb19d655 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -3888,8 +3888,11 @@ bother the user.  They may include
   @code{'no-response-display}      do not display messages in @strong{response} buffer
   @code{'no-error-display}         do not display errors/take error action
   @code{'no-goals-display}         do not goals in @strong{goals} buffer
+  @code{'keep-response}            do not erase the response buffer when goals are shown
   @code{'proof-tree-show-subgoal}  item inserted by the proof-tree package
   @code{'priority-action}          item added via @code{proof-add-to-priority-queue}
+  @code{'empty-action-list}        @code{proof-shell-empty-action-list-command} should not be
+                            called if this is the last item in the action list
 @end lisp
 Note that @code{'invisible} does not imply any of the others. If flags
 are non-empty, interactive cues will be surpressed. (E.g.,
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index f7cb9b3c7..0bba1553c 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -79,7 +79,7 @@ May enable proof-by-pointing or similar features.
 ;;
 ;; Goals buffer processing
 ;;
-(defun pg-goals-display (string keepresponse)
+(defun pg-goals-display (string keepresponse nodisplay)
   "Display STRING in the `proof-goals-buffer', properly marked up.
 Converts term substructure markup into mouse-highlighted extents.
 
@@ -90,7 +90,13 @@ function tries to do that by calling `pg-response-maybe-erase'.
 If KEEPRESPONSE is non-nil, we assume that a response message
 corresponding to this goals message has already been displayed
 before this goals message (see `proof-shell-handle-delayed-output'),
-so the response buffer should not be cleared."
+so the response buffer should not be cleared.
+
+IF NODISPLAY is non-nil, do not display the goals buffer in some
+window (but the goals buffer is updated as described above and
+any window currently showing it will keep it). In two-pane mode,
+NODISPLAY has the effect that the goals are updated but the
+response buffer is displayed."
   ;; Response buffer may be out of date. It may contain (error)
   ;; messages relating to earlier proof states
 
@@ -114,8 +120,11 @@ so the response buffer should not be cleared."
     (set-buffer-modified-p nil)
     
     ;; Keep point at the start of the buffer.
-    (proof-display-and-keep-buffer
-     proof-goals-buffer (point-min))))
+    ;; (For Coq, somebody sets point to the conclusion in the goal, so the
+    ;; position argument in proof-display-and-keep-buffer has no effect.)
+    (unless nodisplay
+      (proof-display-and-keep-buffer
+       proof-goals-buffer (point-min)))))
 
 ;;
 ;; Actions in the goals buffer
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 4de85ddf9..4a97346b5 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -38,6 +38,8 @@
 ;;         -> proof-shell-process-urgent-message
 ;;      -> proof-shell-filter-manage-output
 ;;         -> proof-shell-handle-immediate-output
+;;            -> proof-shell-handle-error-or-interrupt
+;;               -> proof-shell-error-or-interrupt-action
 ;;         -> proof-shell-exec-loop
 ;;            -> proof-tree-check-proof-finish
 ;;            -> proof-shell-handle-error-or-interrupt
@@ -113,8 +115,11 @@ bother the user.  They may include
   'no-response-display      do not display messages in *response* buffer
   'no-error-display         do not display errors/take error action
   'no-goals-display         do not goals in *goals* buffer
+  'keep-response            do not erase the response buffer when goals are shown
   'proof-tree-show-subgoal  item inserted by the proof-tree package
   'priority-action          item added via proof-add-to-priority-queue
+  'empty-action-list        proof-shell-empty-action-list-command should not be
+                            called if this is the last item in the action list
 
 Note that 'invisible does not imply any of the others. If flags
 are non-empty, interactive cues will be surpressed. (E.g.,
@@ -1070,7 +1075,9 @@ being processed."
 	 (unless (eq proof-shell-busy queuemode)
 	   (proof-debug
 	    "proof-append-alist: wrong queuemode detected for busy shell")
-	   (cl-assert (eq proof-shell-busy queuemode)))))
+	   (cl-assert
+            (eq proof-shell-busy queuemode) nil
+            "wrong queuemode in proof-add-to-queue: %s instead expected %s"))))
 
 
   (let ((nothingthere (null proof-action-list)))
@@ -1814,7 +1821,9 @@ i.e., 'goals or 'response."
 	    (buffer-substring-no-properties rstart gmark)))
        ;; display goals output second so it persists in 2-pane mode
        (unless (memq 'no-goals-display flags)
-	 (pg-goals-display proof-shell-last-goals-output both))
+	 (pg-goals-display proof-shell-last-goals-output
+                           (or both (member 'keep-response flags))
+                           (member 'keep-response flags)))
        ;; indicate a goals output has been given
        'goals))