[nongnu] elpa/proof-general 3b765b4 3/5: Adding tests for #597.

[ELPA Syncer]

branch: elpa/proof-general
commit 3b765b48ce7920cbd5a9a8771ee2d4905a901c47
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@cnam.fr>

    Adding tests for #597.
---
 ci/coq-tests.el    | 38 ++++++++++++++++++++++++++++++++++++++
 ci/test_stepwise.v | 16 ++++++++++++++++
 2 files changed, 54 insertions(+)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index fb5635f..160312c 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -303,6 +303,44 @@ For example, COMMENT could be (*test-definition*)"
    'show-proof-stepwise 'diffs-on))
  
 
+(ert-deftest 090_coq-test-regression-Fail()
+  "Test for Fail"
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.v")
+   (lambda ()
+     (coq-test-goto-before "(*FailNoTrace*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (proof-assert-next-command-interactive) ;; pas the comment
+     (proof-assert-next-command-interactive)
+     (proof-shell-wait)
+     (if (coq--version< (coq-version) "8.10.0")
+         (coq-should-buffer-string "The command has indeed failed with message:
+In nested Ltac calls to \"now (tactic)\" and \"easy\", last call failed.
+Tactic failure: Cannot solve this goal.")
+       (coq-should-buffer-string "The command has indeed failed with message:
+Tactic failure: Cannot solve this goal." "*coq*")))))
+
+
+;; (coq-should-buffer-regexp (regexp-quote "The command has indeed failed with 
message: Tactic failure: Cannot solve this goal.") "*response*")
+
+(ert-deftest 091_coq-test-regression-Fail()
+  "Test for Fail"
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.v")
+   (lambda ()
+     (coq-test-goto-before "(*FailTrace*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (proof-assert-next-command-interactive) ;; pas the comment
+     (proof-assert-next-command-interactive)
+     (proof-shell-wait)
+     ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show 
Proof."
+     (coq-should-buffer-string "The command has indeed failed with message:
+In nested Ltac calls to \"now (tactic)\" and \"easy\", last call failed.
+Tactic failure: Cannot solve this goal."))))
+ 
+
 (provide 'coq-tests)
 
 ;;; coq-tests.el ends here
diff --git a/ci/test_stepwise.v b/ci/test_stepwise.v
index 3812adb..af451ff 100644
--- a/ci/test_stepwise.v
+++ b/ci/test_stepwise.v
@@ -11,6 +11,22 @@ Proof using .
   exact proof_of_A.
 Qed. (*test-lemma*)
 
+Section failSection.
+  Local Unset Ltac Backtrace.
+  Goal False.
+  Proof. (*FailNoTrace*)
+    Fail (now auto).
+    auto.
+  Abort.
+
+  Local Set Ltac Backtrace.
+  Goal False. (*FailTrace*) 
+    Fail (now auto).
+    auto.
+  Abort.
+End failSection.
+
+
 Lemma false_proof : forall A B : bool, A = B. 
 Proof.
   intros A B.