diff options
| author | Anaclet | 2020-05-28 11:31:03 +0200 |
|---|---|---|
| committer | Anaclet | 2020-05-29 11:07:09 +0200 |
| commit | cc4b4f6cd626cc6a2f02d3e4efe95dc84d577e3b (patch) | |
| tree | b36396606007312a63e927820170696754d1c45b /ci | |
| parent | 5b1b8ac75056773b4452ce7a41518258010b2bbe (diff) | |
Fix the test 081
Diffstat (limited to 'ci')
| -rw-r--r-- | ci/coq-tests.el | 5 |
1 files changed, 4 insertions, 1 deletions
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)) |