diff options
Diffstat (limited to 'ci')
| -rw-r--r-- | ci/coq-tests.el | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 1a281521..cc60f8a0 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -189,6 +189,17 @@ For example, COMMENT could be (*test-definition*)" (coq-should-response "trois is defined")))) +(ert-deftest 021_coq-test-regression-goto-point () + "Regression test for proof-goto-point after a comment, PR #90" + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") + (lambda () + (coq-test-goto-after "(*test-definition*)") + (proof-goto-point) + (proof-shell-wait) + t))) + + (ert-deftest 030_coq-test-position () "Test locked region after Qed." (coq-fixture-on-file |