Merge PR #10966: `assert_succeeds`&`assert_fails`: multisuccess fix

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48

6 files changed, 31 insertions, 4 deletions

diff --git a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst
new file mode 100644
index 0000000000..09bef82c80
--- /dev/null
+++ b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst
@@ -0,0 +1,11 @@
+- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now
+  only run their tactic argument once, even if it has multiple
+  successes.  This prevents blow-up and looping from using
+  multisuccess tactics with :tacn:`assert_succeeds`.  (`#10966
+  <https://github.com/coq/coq/pull/10966>`_ fixes `#10965
+  <https://github.com/coq/coq/issues/10965>`_, by Jason Gross).
+
+- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now
+  behave correctly when their tactic fully solves the goal.  (`#10966
+  <https://github.com/coq/coq/pull/10966>`_ fixes `#9114
+  <https://github.com/coq/coq/issues/9114>`_, by Jason Gross).
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 79eddbd3b5..6efc634087 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -516,7 +516,9 @@ Coq provides a derived tactic to check that a tactic *fails*:
 .. tacn:: assert_fails @ltac_expr
    :name: assert_fails
 
-   This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`.
+   This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and
+   behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr`
+   has at least one success.
 
 Checking the success
 ~~~~~~~~~~~~~~~~~~~~
@@ -528,7 +530,7 @@ success:
    :name: assert_succeeds
 
    This behaves like
-   :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`.
+   :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`.
 
 Solving
 ~~~~~~~
diff --git a/test-suite/bugs/closed/bug_9114.v b/test-suite/bugs/closed/bug_9114.v
new file mode 100644
index 0000000000..2cf91c1c2b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9114.v
@@ -0,0 +1,5 @@
+Goal True.
+  assert_succeeds (exact I).
+  idtac.
+  (* Error: No such goal. *)
+Abort.
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 19c9fc4423..70427220ed 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -6,3 +6,4 @@ The command has indeed failed with message:
 H is already used.
 The command has indeed failed with message:
 H is already used.
+a
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index fa12f09a46..96b6d652c9 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -22,3 +22,11 @@ intros H.
 Fail intros [H%myid ?].
 Fail destruct 1 as [H%myid ?].
 Abort.
+
+
+(* Test that assert_succeeds only runs a tactic once *)
+Ltac should_not_loop := idtac + should_not_loop.
+Goal True.
+  assert_succeeds should_not_loop.
+  assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *)
+Abort.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index ad6f1765a3..6de9f8f88d 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -325,9 +325,9 @@ Ltac time_constr tac :=
 (** Useful combinators *)
 
 Ltac assert_fails tac :=
-  tryif tac then fail 0 tac "succeeds" else idtac.
+  tryif (once tac) then gfail 0 tac "succeeds" else idtac.
 Ltac assert_succeeds tac :=
-  tryif (assert_fails tac) then fail 0 tac "fails" else idtac.
+  tryif (assert_fails tac) then gfail 0 tac "fails" else idtac.
 Tactic Notation "assert_succeeds" tactic3(tac) :=
   assert_succeeds tac.
 Tactic Notation "assert_fails" tactic3(tac) :=