branch: elpa/proof-general
commit d8a049f751ed3c1e1a01a585fa3bb9fc3b65e43f
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <pierre.court...@cnam.fr>
Adapting omit-proof to rocq prompt.
---
ci/simple-tests/coq-test-omit-proofs.el | 4 +++-
1 file changed, 3 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..17c10a3eb9 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -134,6 +134,8 @@ In particular, test that with proof-omit-proofs-option
configured:
(or
;; for Coq 8.11 and later
(looking-at "Qed\\.\n\n<prompt>Coq <")
+ ;; for Rocq 9 and later
+ (looking-at "Qed\\.\n\n<prompt>Rocq <")
;; for Coq 8.10 and earlier
;; in 8.9 the message is on 1 line, in 8.10 on 3
(looking-at "Qed\\.\n<infomsg>\n?classic_excluded_middle is defined"))))
@@ -170,7 +172,7 @@ 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 (looking-at "\n<prompt>Coq <") (looking-at "\n<prompt>Rocq
<"))))
;; Check 4: check proof-omitted-proof-face is active at marker 3
(message "4: check proof-omitted-proof-face is active at marker 3")
