From ff9b5b11b4266b9260b74d772ae2e5848221f6f8 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 20 May 2020 21:11:27 +0200
Subject: test: Add regression test (currently failing)

---
 ci/coq-tests.el | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'ci')

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
-- 
cgit v1.2.3