diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 15:09:30 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 15:09:30 +0100 |
| commit | d04f262f4c27a086b9ddfef1931586ef1062614d (patch) | |
| tree | 14c13f9879e6c92561627e6308ba6801ea2ed2b6 /theories | |
| parent | 2069c0aec44a50031e33bcb9f7d86c1535ef6b84 (diff) | |
| parent | aa95d82692684a416d7a1c25fce38b4eca1e49c9 (diff) | |
Merge PR #6820: Tacticals assert_fails and assert_succeeds
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Tactics.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 9e6c26b10..8df533e74 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -255,6 +255,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)] @@ -310,8 +311,20 @@ 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 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. |