diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Tactics.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 47a971ef0..287b44fd0 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -313,3 +313,14 @@ Ltac time_constr tac := let ret := tac () in let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in ret. + +(** Useful combinators *) + +Ltac assert_fails tac := + tryif tac then fail 0 tac "succeeds" else idtac. +Ltac assert_succeeds tac := + tryif (assert_fails tac) then fail 0 tac "fails" else idtac. +Tactic Notation "assert_succeeds" tactic3(tac) := + assert_succeeds tac. +Tactic Notation "assert_fails" tactic3(tac) := + assert_fails tac. |