Commit cb1aff4b authored by Robbert Krebbers's avatar Robbert Krebbers

More descriptive test name.

parent d3ad73ff
......@@ -299,7 +299,7 @@ Lemma test_iIntros_let P :
Q, let R := emp%I in P - R - Q - P Q.
Proof. iIntros (Q R) "$ _ $". Qed.
Lemma test_foo P Q : <affine> (Q P) - <affine> Q - <affine> P.
Lemma test_iNext_iRewrite P Q : <affine> (Q P) - <affine> Q - <affine> P.
Proof.
iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment