diff options
| author | Erik Martin-Dorel | 2020-05-20 21:11:27 +0200 |
|---|---|---|
| committer | Anaclet | 2020-05-29 11:05:58 +0200 |
| commit | ff9b5b11b4266b9260b74d772ae2e5848221f6f8 (patch) | |
| tree | 2f77cbd19ba94c827a1734fd6e0761608763d0c6 | |
| parent | 22681a3caf2c8f45700585ea74dffbf48bb2ac19 (diff) | |
test: Add regression test (currently failing)
| -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 |