Commit e78dfb5f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove old debugging code.

parent 09722955
......@@ -830,7 +830,6 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| false => go H pat; find_pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
| _ => fail "hallo" pats
end in
let pats := intro_pat.parse pat in
find_pat false pats.
Supports Markdown
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