diff options
Diffstat (limited to 'src/Util/Tactics/Test.v')
| -rw-r--r-- | src/Util/Tactics/Test.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/Tactics/Test.v b/src/Util/Tactics/Test.v new file mode 100644 index 000000000..63529bbfc --- /dev/null +++ b/src/Util/Tactics/Test.v @@ -0,0 +1,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 *)). |