Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
This fixes the bug that when having: iDestruct (foo with "H") as "{H1 H2} #[H1 H2]" The hypothesis H would not be kept.Robbert Krebbers authoredThis fixes the bug that when having: iDestruct (foo with "H") as "{H1 H2} #[H1 H2]" The hypothesis H would not be kept.
