diff options
| author | Jason Gross | 2019-10-29 12:47:53 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-10-29 12:47:53 -0400 |
| commit | b213691875112530a8d491caff942a761c6508ea (patch) | |
| tree | 44f6c91dd445aededf68a0567de7836c7a44a906 /theories/Init | |
| parent | c9adfcd356f2563d7c4b3927669a8268f184ec24 (diff) | |
Use a less kludgy way of solving #9114
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Tactics.v | 4 |
1 files 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) := |