Commit 2cc0d098 authored by Armaël Guéneau's avatar Armaël Guéneau
Browse files

add tests for edge cases in iDestruct's name reuse

parent 77d152a7
......@@ -1497,4 +1497,21 @@ Proof.
iFrame select _.
Qed.
Lemma test_iDestruct_split_reuse_name P Q :
P Q - P Q.
Proof.
iIntros "H".
iDestruct "H" as "[? H]". Undo.
iDestruct "H" as "[H ?]". Undo.
auto.
Qed.
Lemma test_iDestruct_split_reuse_name_2 P Q R :
(P Q) R - (P Q) R.
Proof.
iIntros "H".
iDestruct "H" as "[[H H'] ?]". Undo.
auto.
Qed.
End tactic_tests.
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