Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
Otherwise, the tactic will fail subsequently. Besides, it was inconsistent w.r.t. the iLöb tactic, which was already doing this.
Robbert Krebbers authoredOtherwise, the tactic will fail subsequently. Besides, it was inconsistent w.r.t. the iLöb tactic, which was already doing this.
