From ccb7bd2948e9bd84997f3461257b2ce1c7ad3e6a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 23 Feb 2018 11:14:54 +0100 Subject: Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross). --- theories/Init/Tactics.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'theories') 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. -- cgit v1.2.3