Message fix

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 (if (coq--version< (coq-version) "9.2alpha") :failed :passed)
   "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 (if (coq--version< (coq-version) "9.2alpha") :failed :passed)
   "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 (if (coq--version< (coq-version) "9.2alpha") :failed :passed)
   "Test for Fail"
   (coq-fixture-on-file
    (coq-test-full-path "test_stepwise.v")

ci/test.sh

@@ -36,4 +36,5 @@ form="(progn (add-to-list 'load-path \"$rootdir\")
 (add-to-list 'load-path \"$srcdir\")
 (setq coq-test-dir \"$srcdir/\"))"  # we need a trailing slash here
 
+
 assert emacs --batch -l ert --eval "$form" -l init-tests.el -l proof-general.el -l coq-tests.el -f ert-run-tests-batch-and-exit

coq/coq-system.el

@@ -150,7 +150,10 @@ This function must not rely on coq-autodetect-version, it would be a cycle."
         (with-temp-buffer
           (setq retv (apply 'process-file process-args))
           (if (or (not expectedretv) (equal retv expectedretv)) (buffer-string)))
-      (error nil))))
+      (error
+       (message "Warning: No Coq/Rocq version detected yet.")
+       (message "ProofGeneral will not be able to start a prover session until you have one in your path.")
+       nil))))
 
 (defun coq-autodetect-version (&optional interactive-p)
   "Detect and record the version of Coq currently in use.
@@ -171,12 +174,13 @@ Interactively (with INTERACTIVE-P), show that number."
     (setq coq-autodetected-help (or coq-output ""))))
 
 (defun coq--version< (v1 v2)
-  "Compare Coq versions V1 and V2."
+  "Compare Coq versions V1 and V2.
+If V1 or V2 is not a valid version number, return nil."
   ;; -snapshot is only supported by Emacs 24.5, not 24.3
   (let ((version-regexp-alist `(("^[-_+ ]?snapshot$" . -4)
                                 ("^pl$" . 0)
                                 ,@version-regexp-alist)))
-    (version< v1 v2)))
+    (condition-case nil (version< v1 v2) (error nil))))
 
 (defcustom coq-pre-v85 nil
   "Deprecated.

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