branch: elpa/proof-general
commit fc4f823e5c7f1c2dc0c3fc429804c60457338219
Author: Hendrik Tews <[email protected]>
Commit: Hendrik Tews <[email protected]>
simple-tests: fix tests for Rocq 9
---
ci/simple-tests/coq-test-omit-proofs.el | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/ci/simple-tests/coq-test-omit-proofs.el
b/ci/simple-tests/coq-test-omit-proofs.el
index 20a54b6e82..f2ec735eb2 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -132,6 +132,8 @@ In particular, test that with proof-omit-proofs-option
configured:
;; There should be a Qed with no error or message after it
(should
(or
+ ;; for Rocq 9.0
+ (looking-at "Qed\\.\n\n<prompt>Rocq <")
;; for Coq 8.11 and later
(looking-at "Qed\\.\n\n<prompt>Coq <")
;; for Coq 8.10 and earlier
@@ -170,7 +172,11 @@ In particular, test that with proof-omit-proofs-option
configured:
(should (search-forward "</infomsg>" nil t))
(forward-line 1))
;; no other messages or errors before the next prompt
- (should (looking-at "\n<prompt>Coq <")))
+ (should (or
+ ;; for Rocq
+ (looking-at "\n<prompt>Rocq <")
+ ;; for Coq
+ (looking-at "\n<prompt>Coq <"))))
;; Check 4: check proof-omitted-proof-face is active at marker 3
(message "4: check proof-omitted-proof-face is active at marker 3")
