• Robbert Krebbers's avatar
    Use `notypeclasses refine` in `iPoseProof` helpers. · 97deecba
    Robbert Krebbers authored
    Also, rewrite `iIntoEmpValid`. Now, instead of using Ltac to traverse
    the type of the term and generate goals for the premises, we repeatedly
    apply a series of lemmas. This has the advantage that it works up to
    convertability, and we no longer need the `eval ...` hacks.
saved_prop.v 5.41 KB