From c59815c860a11948359e96ecc51d566bb5e5d8fb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 25 Oct 2019 15:28:37 -0400
Subject: `assert_succeeds`&`assert_fails`: multisuccess fix

These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.

Fixes #10965
---
 theories/Init/Tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index ad6f1765a3..d26dbe55d1 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -325,7 +325,7 @@ Ltac time_constr tac :=
 (** Useful combinators *)
 
 Ltac assert_fails tac :=
-  tryif tac then fail 0 tac "succeeds" else idtac.
+  tryif once tac then fail 0 tac "succeeds" else idtac.
 Ltac assert_succeeds tac :=
   tryif (assert_fails tac) then fail 0 tac "fails" else idtac.
 Tactic Notation "assert_succeeds" tactic3(tac) :=
-- 
cgit v1.2.3


From c9adfcd356f2563d7c4b3927669a8268f184ec24 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 26 Oct 2019 00:46:14 -0400
Subject: Fix #9114, assert_succeeds (exact I) solves goal

---
 theories/Init/Tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index d26dbe55d1..b2ace39e22 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -325,7 +325,7 @@ Ltac time_constr tac :=
 (** Useful combinators *)
 
 Ltac assert_fails tac :=
-  tryif once tac then fail 0 tac "succeeds" else idtac.
+  tryif (enough True as _; [ once tac | ]) then fail 0 tac "succeeds" else idtac.
 Ltac assert_succeeds tac :=
   tryif (assert_fails tac) then fail 0 tac "fails" else idtac.
 Tactic Notation "assert_succeeds" tactic3(tac) :=
-- 
cgit v1.2.3


From b213691875112530a8d491caff942a761c6508ea Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 29 Oct 2019 12:47:53 -0400
Subject: Use a less kludgy way of solving #9114

---
 theories/Init/Tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories')

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index b2ace39e22..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 (enough True as _; [ once 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) :=
-- 
cgit v1.2.3