Skip to content

Make iDestruct consume wands when it's supposed to

Tej Chajed requested to merge tchajed/iris: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.

Merge request reports