theories/proofmode/tactics.v · 211c2363dec227654c71e72fad02e7a97484afcc · Abhishek Anand / Iris

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago

Improve `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 (_)`.

211c2363

History

Improve `iIntros "_"`.

Robbert Krebbers authored 8 years ago

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 (_)`.