blob: 09985ad73b8630fd51ed84e73d2a0f259ef8f737 (
plain)
1
2
3
4
|
Require Import Crypto.Util.Tactics.Test.
(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds").
|