Skip to content

Clean up `tests/ipm_paper`.

Robbert Krebbers requested to merge robbert/clean_test_ipm_paper into master

The current iInv tactic implements exactly the rule that is in the paper, so let us use that instead of a custom lemma. Back in the days, the iInv tactic would put an update modality in the context, so that did not match the paper.

Merge request reports