Skip to content
GitLab

Make iDestruct consume wands when it's supposed to

Merged Tej Chajed requested to merge tchajed/iris-coq:fix-idestruct-specialize into master

iDestruct ("H" with "HP") where "H" is persistent is supposed to consume "H" if it isn't a forall. Due to a bug in the tactic, this behavior was never triggered and "H" was always left alone.