• Robbert Krebbers's avatar
    Optimize wp_apply and improve its error reporting. · 211dc7ca
    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.
    211dc7ca
proofmode.v 11.1 KB