diff options
| -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 |