-
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.
0429c257
This fixes the bug that when having: iDestruct (foo with "H") as "{H1 H2} #[H1 H2]" The hypothesis H would not be kept.