add test

ProofGeneral · May 4, 2020 · 4f25bf7 · 4f25bf7
1 parent 5900b15
commit 4f25bf7
Showing 1 changed file with 12 additions and 0 deletions.
diff --git 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