diff options
| author | Cyril Anaclet | 2020-05-04 17:12:14 +0200 |
|---|---|---|
| committer | Cyril Anaclet | 2020-05-04 17:12:28 +0200 |
| commit | 4f25bf77571205bcc32d6d2cbf00d516c670243c (patch) | |
| tree | 82f35edf4fb265373bea4a60b7f7591d19754b24 | |
| parent | 5900b15ec4dc6fd344c641c2d676157be70bd551 (diff) | |
add test
| -rw-r--r-- | ci/coq-tests.el | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/ci/coq-tests.el b/ci/coq-tests.el index ac97a110..015b831e 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -242,6 +242,18 @@ For example, COMMENT could be (*test-definition*)" (proof-shell-wait) (should (equal (proof-queue-or-locked-end) proof-point)))))) + +(ert-deftest 070_coq-test-regression-wholefile-no-proof () + "Regression test for no proof bug" + (coq-fixture-on-file + (coq-test-full-path "test_wholefile.v") + (lambda () + (proof-process-buffer) + (proof-shell-wait) + (goto-char (point-min)) + (insert "(*.*)") + (should (equal (proof-queue-or-locked-end) 1))))) + (provide 'coq-tests) ;;; coq-tests.el ends here |