From e53c26994beab53eb36dc34bfef335abcad07d47 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 5 Feb 2020 17:43:55 +0100
Subject: [PATCH] Add tests for the `-# pat` intro pattern.

---
 tests/proofmode.ref | 23 +++++++++++++++++++++++
 tests/proofmode.v   | 15 +++++++++++++++
 2 files changed, 38 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 93b90699c..be894c20a 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -54,6 +54,29 @@
   --------------------------------------â–¡
   <affine> (P ∗ Q)
   
+"test_iDestruct_spatial"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Q : PROP
+  ============================
+  "HQ" : <affine> Q
+  --------------------------------------∗
+  Q
+  
+"test_iDestruct_spatial_affine"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Q : PROP
+  Affine0 : Affine Q
+  ============================
+  "HQ" : Q
+  --------------------------------------∗
+  Q
+  
 The command has indeed failed with message:
 Ltac call to "done" failed.
 No applicable tactic.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b41edc481..fc1e7df41 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -90,6 +90,21 @@ Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persisten
   Q ∗ (Q -∗ P) -∗ P ∗ Q.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
 
+Check "test_iDestruct_spatial".
+Lemma test_iDestruct_spatial Q : □ Q -∗ Q.
+Proof. iIntros "#HQ". iDestruct "HQ" as "-#HQ". Show. done. Qed.
+
+Check "test_iDestruct_spatial_affine".
+Lemma test_iDestruct_spatial_affine Q `{!Affine Q} : □ Q -∗ Q.
+Proof.
+  iIntros "#-#HQ".
+  (* Since [Q] is affine, it should not add an <affine> modality *)
+  Show. done.
+Qed.
+
+Lemma test_iDestruct_spatial_noop Q : Q -∗ Q.
+Proof. iIntros "-#HQ". done. Qed.
+
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
 Proof. iIntros (??) "H". auto. Qed.
 
-- 
GitLab