Skip to content

Use original pattern in iDestruct error messages

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

I also took the liberty of giving a specific error to iDestruct "H" as "[H1 H2 H3]", because that was the actual mistake I made (I wrote iDestruct "H" as "[$H1 H2]" because I keep wanting to name the thing I'm framing, but of course that doesn't really make sense).

Edited by Tej Chajed

Merge request reports