diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 2eaaa0023..520f22c9a 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -299,7 +299,10 @@ For example, COMMENT could be (*test-definition*)" (coq-test-goto-before " (*test-insert*)") (proof-goto-point) (proof-shell-wait) - (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)")) + ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof." + (if (coq--post-v811) + (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)") + (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)"))) 'show-proof-stepwise 'diffs-on))