• Robbert Krebbers's avatar
    Use `notypeclasses refine` in `iPoseProof` helpers. · d5d02af5
    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.