From cc4b4f6cd626cc6a2f02d3e4efe95dc84d577e3b Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Thu, 28 May 2020 11:31:03 +0200
Subject: Fix the test 081

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

(limited to 'ci')

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index da0da3d8..8040b122 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -298,7 +298,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))
  
 
-- 
cgit v1.2.3