Commit 45e4ff7a authored by Joachim Bard's avatar Joachim Bard

Merge branch 'master' of

parents f1d00ce8 42e791ee
......@@ -239,3 +239,13 @@ Ltac destruct_ex H pat :=
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
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment