From 79c6b6ef7cdb04229eec37382a6fa81cb067498a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org>
Date: Sun, 19 Sep 2021 22:55:07 +0200
Subject: [PATCH] add tests for edge cases in iDestruct's name reuse

---
 tests/proofmode.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 31cc46faa..7b2ac9d6b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1633,4 +1633,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.
-- 
GitLab