• Robbert Krebbers's avatar
    Improve iFrame tactic · 43d45c6b
    Robbert Krebbers authored
    - It can now also frame under later.
    - Better treatment of evars, it now won't end up in loops whenever the goal
      involves sub-formulas ?P and it trying to apply all framing rules eagerly.
    - It no longer delta expands while framing.
    - Better clean up of True sub-formulas after a successful frame. For example,
      framing "P" in "▷ ▷ P ★ Q" yields just "Q" instead of "▷ True ★ Q" or so.
    43d45c6b
proofmode.v 1.77 KB