From 5988d449475ffa63349bfd4d2f0e338f525ab464 Mon Sep 17 00:00:00 2001
From: Anaclet <cyril.anaclet@gmail.com>
Date: Thu, 28 May 2020 11:31:03 +0200
Subject: [PATCH] Fix the test 081

---
 ci/coq-tests.el | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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  "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>"))
+     ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof."
+     (if (coq--post-v811)
+	 (coq-should-buffer  "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>")
+       (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)")))
    'show-proof-stepwise 'diffs-on))