Fix the test 081

ProofGeneral · May 28, 2020 · 5988d44 · 5988d44
1 parent 19c7a72
commit 5988d44
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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))