Commit 42e791ee authored by Heiko Becker's avatar Heiko Becker

Add debugging tactics from separate branch

parent 527d291e
......@@ -239,3 +239,13 @@ Ltac destruct_ex H pat :=
end.
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
(* Debugging tactics, if scripts fail *)
Ltac debug_term t :=
let name := fresh "debug" in
let res := (eval compute in t) in
assert (t = res) as name by (vm_compute; auto);
rewrite name; clear name.
Ltac step f :=
cbn iota beta delta [f].
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