blob: 63529bbfc81d944a6c424f6201835a597d0210c9 (
plain)
1
2
3
|
(** Test if a tactic succeeds, but always roll-back the results *)
Tactic Notation "test" tactic3(tac) :=
try (first [ tac | fail 2 tac "does not succeed" ]; fail 0 tac "succeeds"; [](* test for [t] solved all goals *)).
|