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(-)

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