-
Robbert Krebbers authored
In the following ways: - When having `P → Q` it will now also work when the spatial context is non-empty. - When having `∀ x : A, Q` it will now do an `iIntros (_)`.
211c2363
In the following ways: - When having `P → Q` it will now also work when the spatial context is non-empty. - When having `∀ x : A, Q` it will now do an `iIntros (_)`.