From 8e7299440d0dfe990f06b8f94396ca0fce259424 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org>
Date: Fri, 1 Oct 2021 14:21:23 +0200
Subject: [PATCH] Add tests for iIntuitionistic/iSpatial/iModCore on non-fresh
 names

---
 tests/proofmode.ref      |  8 ++++++++
 tests/proofmode.v        | 14 ++++++++++++++
 tests/proofmode_iris.ref |  4 ++++
 tests/proofmode_iris.v   |  7 +++++++
 4 files changed, 33 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index fd5ebf4ad..d03482932 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -752,3 +752,11 @@ Tactic failure: iPure: (φ n) not pure.
      : string
 The command has indeed failed with message:
 Tactic failure: iIntuitionistic: Q not persistent.
+"test_iDestruct_intuitionistic_not_fresh"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntuitionistic: "H" not fresh.
+"test_iDestruct_spatial_not_fresh"
+     : string
+The command has indeed failed with message:
+Tactic failure: iSpatial: "H" not fresh.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7b2ac9d6b..fa820d1ff 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1650,4 +1650,18 @@ Proof.
   auto.
 Qed.
 
+Check "test_iDestruct_intuitionistic_not_fresh".
+Lemma test_iDestruct_intuitionistic_not_fresh P Q :
+  P -∗ □ Q -∗ False.
+Proof.
+  iIntros "H H'". Fail iDestruct "H'" as "#H".
+Abort.
+
+Check "test_iDestruct_spatial_not_fresh".
+Lemma test_iDestruct_spatial_not_fresh P Q :
+  P -∗ Q -∗ False.
+Proof.
+  iIntros "H H'". Fail iDestruct "H'" as "-#H".
+Abort.
+
 End tactic_tests.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index f7d43a2cc..4c4d3a96c 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -168,6 +168,10 @@ Tactic failure: iInv: invariant "H2" not found.
   "H" : own γ 1%Qp
   --------------------------------------∗
   own γ 1%Qp
+"test_iDestruct_mod_not_fresh"
+     : string
+The command has indeed failed with message:
+Tactic failure: iMod: "H" not fresh.
 "test_iInv"
      : string
 1 goal
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 89ac3f556..466099cd2 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -243,6 +243,13 @@ Section iris_tests.
     iExact "H".
   Qed.
 
+  Check "test_iDestruct_mod_not_fresh".
+  Lemma test_iDestruct_mod_not_fresh P Q :
+    P -∗ (|={⊤}=> Q) -∗ (|={⊤}=> False).
+  Proof.
+    iIntros "H H'". Fail iDestruct "H'" as ">H".
+  Abort.
+
 End iris_tests.
 
 Section monpred_tests.
-- 
GitLab