Commit 124cb845 authored by Heiko Becker's avatar Heiko Becker

Push changed Ltacs file forgotten by last commit

parent da70f298
......@@ -168,3 +168,15 @@ Ltac telling_rewrite pat hyp :=
Tactic Notation "unify asm" open_constr(pat) hyp(H):=
telling_rewrite pat H.
Ltac destruct_ex H pat :=
match type of H with
| exists v, ?H' =>
let vFresh:=fresh v in
let fN := fresh "ex" in
destruct H as [vFresh fN];
destruct_ex fN pat
| _ => destruct H as pat
end.
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment