• 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
Name
Last commit
Last update
algebra Loading commit data...
benchmark Loading commit data...
docs Loading commit data...
heap_lang Loading commit data...
prelude Loading commit data...
program_logic Loading commit data...
proofmode Loading commit data...
tests Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
naming.txt Loading commit data...