diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-23 11:14:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-28 19:44:38 +0100 |
| commit | ccb7bd2948e9bd84997f3461257b2ce1c7ad3e6a (patch) | |
| tree | 4c9604bcaec5d10b3cc94c70df9b78991ec79a59 /theories | |
| parent | 0c5f0afffd37582787f79267d9841259095b7edc (diff) | |
Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).
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. |