Add tests for iIntuitionistic/iSpatial/iModCore on non-fresh names

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.

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.

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

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.