• 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
coq_tactics.v 34.5 KB