Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
It not behaves more consistently with iExact and thus also works in the case H : P -★ □^n Q |- Q.
Robbert Krebbers authoredIt not behaves more consistently with iExact and thus also works in the case H : P -★ □^n Q |- Q.
