Rocq: enable messages for Rocq >= 9.2

Disable Set Silent for Rocq >= 9.2, which does not print any goals any
more. See also PR 21038 for Rocq.

Fixes #842 #849 #843

Author: hendriktews

ci/coq-tests.el

@@ -202,7 +202,7 @@ For example, COMMENT could be (*test-definition*)"
 
 (ert-deftest 020_coq-test-definition ()
   ;; There are no infomsgr when running silent.
-  :expected-result :failed
+  ;; :expected-result :failed
   "Test *response* output after asserting a Definition."
   (coq-fixture-on-file
    (coq-test-full-path "test_stepwise.v")
@@ -401,7 +401,7 @@ For example, COMMENT could be (*test-definition*)"
   ;; 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
+  ;;:expected-result :failed
   "Test for Fail"
   (coq-fixture-on-file
    (coq-test-full-path "test_stepwise.v")
@@ -429,7 +429,7 @@ For example, COMMENT could be (*test-definition*)"
   ;; 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
+  ;;:expected-result :failed
   "Test for Fail"
   (coq-fixture-on-file
    (coq-test-full-path "test_stepwise.v")

coq/coq.el

@@ -141,7 +141,10 @@ Namely, goals that do not fit in the goals window."
      ;; keeping the current value (that may come from another file).
      ,(format "Add Search Blacklist %s." coq-search-blacklist-current-string))
    '("Set Suggest Proof Using.")
-   (if coq-run-completely-silent '("Set Silent.") ())
+   (if (and coq-run-completely-silent
+            (coq--version< (coq-version t) "9.2+alpha"))
+       '("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