diff options
Diffstat (limited to 'theories/Init/Tactics.v')
| -rw-r--r-- | theories/Init/Tactics.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index a92d9b1ef..58827eefb 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -88,6 +88,14 @@ Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) := Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) := try intros until n; destruct n as []_eqn:H. +(** Break every hypothesis of a certain type *) + +Ltac destruct_all t := + match goal with + | x : t |- _ => destruct x; destruct_all t + | _ => idtac + end. + (* Rewriting in all hypothesis several times everywhere *) Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *. |