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 From aa95d82692684a416d7a1c25fce38b4eca1e49c9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 23 Feb 2018 11:20:26 +0100 Subject: Uniform spacing layout in Tactics.v. --- theories/Init/Tactics.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'theories') diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 287b44fd0..c36494c9e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -253,6 +253,7 @@ Tactic Notation "dependent" "induction" ident(H) := writing a version of [inversion] / [dependent destruction] which does not lose information, i.e., does not turn a goal which is provable into one which requires axiom K / UIP. *) + Ltac simpl_proj_exist_in H := repeat match type of H with | context G[proj1_sig (exist _ ?x ?p)] @@ -308,6 +309,7 @@ Ltac inversion_sigma_step := Ltac inversion_sigma := repeat inversion_sigma_step. (** A version of [time] that works for constrs *) + Ltac time_constr tac := let eval_early := match goal with _ => restart_timer end in let ret := tac () in -- cgit v1.2.3