Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
We now first iPoseProof the lemma and instantiate its premises before trying to search for the sub-term where to apply. As a result, instantiation of the premises of the applied lemmas happens only once, instead of it being done for each sub-term as obtained by reshape_expr.
Robbert Krebbers authoredWe now first iPoseProof the lemma and instantiate its premises before trying to search for the sub-term where to apply. As a result, instantiation of the premises of the applied lemmas happens only once, instead of it being done for each sub-term as obtained by reshape_expr.
