Skip to content

Make sure that `iRevert` preserves names and does not invent fresh ones.

Robbert Krebbers requested to merge robbert/iRevert_names into master

Consider:

From iris.proofmode Require Import tactics.

Lemma test_iRevert_order_and_names {PROP : bi} (P1 P2 : PROP) :
  P1 -∗ P2 -∗ P1 ∗ P2.
Proof.
  iIntros "H1 H2". iRevert (P1 P2) "H1 H2".

Previously this would give ∀ a a0 : PROP, a -∗ a0 -∗ a ∗ a0.

With this MR it gives ∀ P1 P2, P1 -∗ P2 -∗ P1 ∗ P2

The new test in this MR also checks that the reverts happen in the right order, i.e., we do not get ∀ P2 P1, P2 -∗ P1 -∗ P1 ∗ P2.

Merge request reports