Skip to content
  • Robbert Krebbers's avatar
    Improve `iIntros "_"`. · 211c2363
    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